|
A Specifier’s Introduction to Formal Methods |
Jeannette M. Wing, Carnegie Mellon University
|
Applied to computer systems development, formal methods provide mathematically based techniques that describe system properties. As such, they present a framework for systematically specifying, developing, and verifying systems. |
Formal methods used in developing computer systems are mathematically based techniques for describing system properties. Such formal methods
provide frameworks within which people can specify, develop, and verify systems in a systematic, rather than ad hoc, manner.
A method is formal if it has a sound mathematical basis. typically given by a formal specification language. This basis provides the means of precisely defining notions like consistency and completeness
and, more relevantly, specification, implementation, and correctness. It provides the means of proving that a specification is realizable, proving that a system has been implemented correctly, and proving properties
of a system without necessarily running it to determine its behavior.
A formal method also addresses a number of pragmatic considerations: who uses it, what it is used for, when it is used, and how it is used. Most commonly, system designers use formal methods to specify a
system’'s desired behavioral and structural properties.
However, anyone involved in any stage of system development can make use of formal methods. They can be used in the initial statement of a customer’'s requirements, through system design, implementation,
testing, debugging, maintenance, verification, and evaluation.
Formal methods are used to reveal ambiguity, incompleteness, and inconsistency in a system. When used early in the system development process, they can reveal design flaws that otherwise might be discovered only during costly testing and debugging phases. When used later, they can help determine the correctness of a system implementation and the equivalence of different implementations.
For a method to be formal, it must have a well-defined mathematical basis. It need not address any pragmatic considerations, but lacking such considerations would render it useless. Hence, a formal method should possess a set of guidelines or a “"style sheet”" that tells the user the circumstances under which the method can and should be applied as well as how it can be applied most effectively.
One tangible product of applying a formal method is a formal specification. A specification serves as a contract, a valuable piece of documentation, and a means of communication among a client, a specifier, and an implementer. Because of their mathematical basis, formal specifications are more precise and usually more concise than informal ones.
Since a formal method is a method and not just a computer program or language, it may or may not have tool support. If the syntax of a formal method’'s specification language is made explicit, providing standard syntax analysis tools for formal specifications would be appropriate. If the language’'s semantics are sufficiently restricted, varying degrees of semantic analysis can be performed with machine aids as well. Thus, formal specifications have the additional advantage over informal ones of being amenable to machine analysis and
manipulation.
For more on the benefits of formal specification, see Meyer. For more on the distinction between a method and a language, and what specifying a computer system means, see Lamport.
What is a specification language?
A formal specification language provides a formal method’s mathematical basis. I borrowed the terms and definitions that follow from Guttag et al. Burstall and Goguen have used the term "language" and more recently the term "institution" for the notion of a formal specification language.
|
Definition: A formal specification language is a triple, <Syn, Sem, Sat>, where Syn and Sem are sets and Sat ⊆ Syri x Sem is a relation between them. Sw is called the language’'s syntactic domain; Sem, its semantic domain; and Sur, its satisfies relation. |
|
Definition: Given a specification language, <Syn, Sem, Sat>, if Sat(syn, sem) then syn is a specification of sem, and sem is a specificand of syn. |
|
Definition: Given a specification language, <Syn, Sem, Sat>, the specificand set of a specification syn in Syn is the set of all specificands sem in Sem such that Sar(sw, sem). |
Less formally, a formal specification language provides a notation (its syntactic domain), a universe of objects (its semantic domain), and a precise rule defining which objects satisfy each specification. A specification is a sentence written in terms of the elements of the syntactic domain. It denotes a specificand set, a subset of the semantic domain. A specificand is an object satisfying a specification. The satisfies relation provides the meaning, or interpretation, for the syntactic elements.
Backus-Naur form is an example of a simple formal specification language, with a set of grammars as its syntactic domain and a set of strings as its semantic domain. Every string is a specificand of each grammar that generates it. Every specificand set is a formal language.
In principle, a formal method is based on some well-defined formal specification language. In practice, however, this language may not have been explicitly given. The more explicit the specification language’'s definition, the more well-defined the formal method.
Formal methods differ because their specification languages have different syntactic and/or semantic domains. Even if they have identical syntactic and semantic domains, they may have different satisfies relations.
Syntactic domains. We usually define a specification language’'s syntactic domain in terms of a set of symbols (for example, constants, variables, and logical connectives) and a set of grammatical rules for combining these symbols into well-formed sentences. For example, using standard notation for universal quantification (V) and logical implication (*), let x be a logical variable and P and Q be predicate symbols. Then this sentence, Vx.P(x) Q(x), would be well-formed in predicate logic, but this one, Vx. + P(x) 3 Q(x), would not because + is a binary logical connective.
A syntactic domain need not be restricted to text; graphical elements such as boxes, circles, lines, arrows, and icons can be given a formal semantics just as precisely as textual ones. A well-formedness condition on such a visual specification might be that all arrows start and stop at boxes.
Semantic domains. Specification languages differ most in their choice of semantic domain. The following are some examples:
•Abstract-data-type specification languages are used to specify algebras, theories, and programs. Though specifications written in these languages range over different semantic domains, they often look syntactically similar.
•Concurrent and distributed systems specification languages are used to specify state sequences, event sequences, state and transition sequences, streams, synchronization trees, partial orders, and state machines.
•Programming languages are used to specify functions from input to output, computations, predicate transformers, relations, and machine instructions.
Each programming language (with a welldefined formal semantics) is a specification language, but the reverse is not true, because specifications in general do not have to be executable on some machine whereas programs do. By using a more abstract specification language, we gain the advantage of not being restricted to expressing only computable functions. It is perfectly reasonable in a specification to express notions like “"Forallxin set A, there exists ay in setB such that property P holds
of.randy,”"whereA andBmightbeinfinite
sets.
Programs, however, are formal objects,
susceptible to formal manipulation (for
example, compilation and execution). Thus,
programmers cannot escape from formal
methods. The question is whether they work
with informal requirements and formal
programs, or whether they use additional
formalism to assist them during requirements
specification.
When a specification language’'s semantic
domain is over programs or systems of
programs, the term implements is used for
the satisfies relation, and the term implementation
is used for a specificand in Sem.
An implementation prog is correct with
respect to a given specification spec ifprog
satisfies spec. More formally,
Definition: Given a specification language,
<Syn, Sem, Sat>, an implementation prog in
Sem is correct with respect to a given
specification specin Syn if andonly ifSar(spec,
pro&?).
Satisfies relation. We often would like
to specify different aspects of a single
specificand, perhaps using different specification
languages. For example, you might
want to specify the functional behavior of
a collection of program modules as the
composition of the functional behaviors of
the individual modules. You might additionally
want to specify a structural relationship
between the modules such as what
set of modules each module directly invokes.
To accommodate these different views
of a specificand, we first associate with
each specification language a semantic
abstraction function, which partitions
specificands into equivalence classes.
Definition: Given a semantic domain, Srm, a
semantic abstraction function is a
homomorphism, A: Sem 4 z5“"”",th at maps
elements of the semantic domain into
equivalence classes.
For a given specification language, we
choose a semantic abstraction function to
induce an abstract satisfies relation between
specifications and equivalence classes of
specificands. This relation defines a view
on specificands.
Definition: Given a specification language,
<Sjn, Sem, Sat>, and a semantic abstraction
function, A, defined on Sem, an abstract
satisfies relation, ASat:Syn + 2‘'“"”", is the
induced relation such that
Vspec E Synpog E Sem
[Sat(spec,prog) = ASut(spec,A(prog))]
Different semantic abstraction functions
make it possible to describe multiple views
of the same equivalence class of systems,
or similarly, impose different kinds of constraints
on these systems. Having several
specification languages with different semantic
abstraction functions for a single
semantic domain can be useful. This encourages
and supports complementary
specifications of different aspects of a system
A Specifier's Introduction to Formal Methods.hwp