Formal methods 161883 223875315 2008-07-06T08:05:47Z 84.101.10.34 /* Formal methods and notations */ In [[computer science]] and [[software engineering]], '''formal methods''' are particular kind of [[mathematically]]-based techniques for the [[formal specification|specification]], development and [[formal verification|verification]] of [[software]] and [[hardware]] systems.<ref name="butler">{{cite web|author=R. W. Butler|title=What is Formal Methods?|url=http://shemesh.larc.nasa.gov/fm/fm-what.html|date=2001-08-06|accessdate=2006-11-16}}</ref> 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.<ref>{{cite paper|author=C. Michael Holloway|title=Why Engineers Should Consider Formal Methods|url=http://klabs.org/richcontent/verification/holloway/nasa-97-16dasc-cmh.pdf| publisher=16th Digital Avionics Systems Conference (27-30 October 1997)|accessdate=2006-11-16}}</ref> However, the high cost of using formal methods means that they are usually only used in the development of high-integrity systems, where [[safety]] or [[security]] is important. ==Uses== Formal methods can be applied at various points through the [[software development process|development process]]. (For convenience, we use terms common to the [[waterfall model]], though any development process could be used.) ===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 [[Backus-Naur 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. ===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 [[assertion (computing)|assertion]]s in the executable code. ===Verification=== Once a formal specification has been developed, the specification may be used as the basis for [[mathematical proof|proving]] properties of the specification (and hopefully by inference the developed system). ====Human-directed proof==== Sometimes, the motivation for proving the correctness of a system is not the obvious need for re-assurance 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 low-level 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. ====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 human-produced 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 such systems are like [[Oracle machine|oracle]]s: 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. ==Criticisms== The field of formal methods has its critics. At the current state of the art, proofs of correctness, whether handwritten or computer-assisted, 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 the benefits of having such proofs, or the danger in having undetected errors, makes them worth the resources. Example: in [[aerospace engineering]], undetected errors may cause [[death]], so formal methods are more popular than in other application areas. At times, proponents of formal methods have claimed that their techniques would be the [[silver bullet]] to the [[software crisis]]. Of course, it is widely believed that there is [[no silver bullet]] for software development, and some have written off formal methods due to those overstated, overreaching claims. ==Formal methods and notations== There are a variety of formal methods and notations available, including * [[Abstract State Machines]] (ASMs) * [[Alloy language|Alloy]] * [[B-Method]] * [[Process calculi]] ** [[Communicating Sequential Processes|CSP]] ** [[Language Of Temporal Ordering Specification|LOTOS]] ** [[Pi-calculus|π-calculus]] * [[Actor model]] * [[Esterel]] * [[Lustre programming language|Lustre]] * [[mCRL2]] * [[Petri nets]] * [[RAISE specification language|RAISE]] * [[Vienna Development Method|VDM]] ** [[VDM specification language|VDM-SL]] ** VDM++ * [[Z notation]] * [[Rebeca Modeling Language]] ==See also== * [[Formal verification]] * [[Formal system]] * [[Automated theorem proving]] * [[Model checking]] * [[Software engineering]] * [[:Category:Software engineering disasters|Software engineering disasters]] * [[:Category:Formal methods people|Formal methods people]] ==References== <div class="references-small"> <references/> </div> ==External links== *[http://www.bmethod.com B Method.com] : his site is designed to present different work and subjects concerning the B method, a formal method with proof * [[Foldoc:formalmethods]] * [http://www.fmeurope.org/ Formal Methods Europe (FME)] * [http://www.fmeurope.org/twiki/bin/view/ FME's wiki on formal methods] * [http://vl.fmnet.info/pubs/ Formal methods publications] * [http://vl.fmnet.info/ Virtual Library formal methods] * [http://vl.fmnet.info/whos-who/ Who's who in formal methods] * [http://vl.fmnet.info/meetings/ Meetings] * [http://vl.fmnet.info/orgs/ Organizations] * [http://vl.fmnet.info/companies/ Companies] <!-- * [http://vl.zuser.org/ Z notation] --> {{FOLDOC}} [[Category:Formal methods| ]] [[Category:Software development philosophies]] [[Category:Formal sciences]] [[de:Formale Methode]] [[fr:Méthode formelle (informatique)]] [[ja:形式手法]] [[pl:Metody formalne]] [[pt:Métodos formais]] [[vi:Các phương pháp hình thức]] [[uk:Формальні методи]]