Formal methods
From Wikipedia, the free encyclopedia
In computer science and software engineering, formal methods are particular kind of mathematicallybased techniques for the specification, development and verification of software and hardware systems.^{[1]} The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analyses can contribute to the reliability and robustness of a design.^{[2]} However, the high cost of using formal methods means that they are usually only used in the development of highintegrity systems,^{[3]} where safety or security is important.
Contents 
[edit] Taxonomy
Formal methods can be used at a number of levels:
Level 0: Formal specification may be undertaken and then a program developed from this informally. This has been dubbed formal methods lite. This may be the most costeffective option in many cases.
Level 1: Formal development and formal verification may be used to produce a program in a more formal manner. For example, proofs of properties or refinement from the specification to a program may be undertaken. This may be most appropriate in highintegrity systems involving safety or security.
Level 2: Theorem provers may be used to undertake fully formal machinechecked proofs. This can be very expensive and is only practically worthwhile if the cost of mistakes is extremely high (e.g., in critical parts of microprocessor design).
Further information on this is expanded below.
As with the subdiscipline of programming language semantics, styles of formal methods may be roughly classified as follows:
 Denotational semantics, in which the meaning of a system is expressed in the mathematical theory of domains. Proponents of such methods rely on the wellunderstood nature of domains to give meaning to the system; critics point out that not every system may be intuitively or naturally viewed as a function.
 Operational semantics, in which the meaning of a system is expressed as a sequence of actions of a (presumably) simpler computational model. Proponents of such methods point to the simplicity of their models as a means to expressive clarity; critics counter that the problem of semantics has just been delayed (who defines the semantics of the simpler model?).
 Axiomatic semantics, in which the meaning of the system is expressed in terms of preconditions and postconditions which are true before and after the system performs a task, respectively. Proponents note the connection to classical logic; critics note that such semantics never really describe what a system does (merely what is true before and afterwards).
[edit] Lightweight formal methods
Some practitioners believe that the formal methods community has overemphasized full formalization of a specification or design.^{[4]}^{[5]} They contend that the expressiveness of the languages involved, as well as the complexity of the systems being modelled, make full formalization a difficult and expensive task. As an alternative, various lightweight formal methods, which emphasize partial specification and focused application, have been proposed. Examples of this lightweight approach to formal methods include the Alloy object modelling notation,^{[6]} Denney's synthesis of some aspects of the Z notation with use case driven development,^{[7]} and the CSK VDM Tools.^{[8]}
[edit] Uses
Formal methods can be applied at various points through the development process. (For convenience, we use terms common to the waterfall model, though any development process could be used.)
[edit] Specification
Formal methods may be used to give a description of the system to be developed, at whatever level(s) of detail desired. This formal description can be used to guide further development activities (see following sections); additionally, it can be used to verify that the requirements for the system being developed have been completely and accurately specified.
The need for formal specification systems has been noted for years. In the ALGOL 60 Report, John Backus presented a formal notation for describing programming language syntax (later named Backus normal form or BackusNaur form (BNF)); Backus also described the need for a notation for describing programming language semantics. The report promised that a new notation, as definitive as BNF, would appear in the near future; it never appeared.
[edit] Development
Once a formal specification has been developed, the specification may be used as a guide while the concrete system is developed (i.e. realized in software and/or hardware). Examples:
 If the formal specification is in an operational semantics, the observed behavior of the concrete system can be compared with the behavior of the specification (which itself should be executable or simulateable). Additionally, the operational commands of the specification may be amenable to direct translation into executable code.
 If the formal specification is in an axiomatic semantics, the preconditions and postconditions of the specification may become assertions in the executable code.
[edit] Verification
Once a formal specification has been developed, the specification may be used as the basis for proving properties of the specification (and hopefully by inference the developed system).
[edit] Humandirected proof
Sometimes, the motivation for proving the correctness of a system is not the obvious need for reassurance of the correctness of the system, but a desire to understand the system better. Consequently, some proofs of correctness are produced in the style of mathematical proof: handwritten (or typeset) using natural language, using a level of informality common to such proofs. A "good" proof is one which is readable and understandable by other human readers.
Critics of such approaches point out that the ambiguity inherent in natural language allows errors to be undetected in such proofs; often, subtle errors can be present in the lowlevel details typically overlooked by such proofs. Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.
[edit] Automated proof
In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into two general categories:
 Automated theorem proving, in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical axioms, and a set of inference rules.
 Model checking, in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution.
Neither of these techniques work without human assistance. Automated theorem provers usually require guidance as to which properties are "interesting" enough to pursue; model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model.
Proponents of such systems argue that the results have greater mathematical certainty than humanproduced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners.
Critics note that some of those systems are like oracles: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "verifying the verifier"; if the program which aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification.
[edit] Criticisms
The field of formal methods has its critics. Handwritten proofs of correctness need significant time (and thus money) to produce, with limited utility other than assuring correctness. This makes formal methods more likely to be used in fields where it is possible to perform automated proofs using software, or in cases where the cost of a fault is high. Example: in railway engineering and aerospace engineering, undetected errors may cause death, so formal methods are more popular in this field than in other application areas.
At times, proponents of formal methods^{[who?]} have claimed that their techniques would be the silver bullet to the software crisis. It is widely believed^{[citation needed]} that there is no silver bullet for software development, and some^{[who?]} have written off formal methods due to those overstated, overreaching claims.
[edit] Formal methods and notations
There are a variety of formal methods and notations available, including
 Abstract State Machines (ASMs)
 Alloy
 BMethod
 Common Algebraic Specification Language(CASL)
 Process calculi
 Actor model
 Esterel
 Lustre
 mCRL2
 Petri nets
 RAISE
 VDM
 VDMSL
 VDM++
 Z notation
 Rebeca Modeling Language
 Cleanroom
 SPIN
 PAT is a powerful free model checker, simulator and refinement checker for concurrent systems and CSP extensions (e.g. shared variables, arrays, fairness).
[edit] See also
 Automated theorem proving
 Design by contract
 Formal methods people
 Formal specification
 Formal verification
 Formal system
 Model checking
 Software engineering
 Software engineering disasters
 Specification language
[edit] References
This article was originally based on material from the Free Online Dictionary of Computing, which is licensed under the GFDL.
 ^ R. W. Butler (20010806). "What is Formal Methods?". http://shemesh.larc.nasa.gov/fm/fmwhat.html. Retrieved on 20061116.
 ^ C. Michael Holloway. Why Engineers Should Consider Formal Methods. 16th Digital Avionics Systems Conference (2730 October 1997). http://klabs.org/richcontent/verification/holloway/nasa9716dasccmh.pdf. Retrieved on 20061116.
 ^ M. Archer, C. Heitmeyer and E. Riccobene. Proving invariants of I/O automata with TAME. Automated Software Engineering, 9, 201232 (2002).
 ^ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996
 ^ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering", Crosstalk: The Journal of Defense Software Engineering, January 2003
 ^ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256290
 ^ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, AddisonWesley Professional Publishing, 2005, ISBN 0321316436.
 ^ Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods", In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, SpringerVerlag, October 1998
[edit] External links
 Foldoc:formalmethods
 Formal Methods Wiki
 Formal Methods Europe (FME)
 FME's wiki on formal methods
 Virtual Library formal methods
 Formal methods publications
 Who's who in formal methods

