About Opentopia
Opentopia Directory Encyclopedia Tools

Formal methods

Encyclopedia : F : FO : FOR : Formal methods

In computer science, formal methods refers to mathematically based techniques for the specification, development and verification of software and hardware systems. The approach is especially important in high-integrity systems, for example where safety or security is important, to help ensure that errors are not introduced into the development process. Formal methods are particularly effective early in development at the requirements and specification levels, but can be used for a completely formal development of an implementation (e.g., a program).

Contents

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 cost-effective option in many cases.

Level 1: Formal development and 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 high-integrity systems involving safety or security.

Level 2: Theorem provers may be used to undertake fully formal machine-checked 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 sub-discipline of programming language semantics, styles of formal methods may be roughly classified as follows:

Lightweight formal methods

Some practitioners believe that the formal methods community has overemphasized full formalization of a specification or design (Jackson and Wing 1996),(George and Vaughn 2003). 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 (Jackson 2002), Denney's synthesis of some aspects of the Z notation with use case driven development (Denney 2005), and the IFAD VDM toolset (Agerholm and Larsen 1998).

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.)

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:

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).

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: 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 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.

Criticisms

In addition to the internal criticisms mentioned above, the field of formal methods as a whole 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

See also

References

External links

This article was originally based on material from the Free On-line Dictionary of Computing, which is [Foldoc licenselicensed] under the GFDL.

 

From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.

Search Titles
0123456789
ABCDEFGHIJ
KLMNOPQRST
UVWXYZ?

E-mail this article to:

Personal Message: