Formal methods

Formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Overview

Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.

Specification

Formal methods can be used at a number of levels:

• Level 0: Formal syntax and semantics for a programming language, but with conventional mathematical semantics. This may include a step called formal specification where an unambiguous and consistent definition of the functions to be provided are developed.

• Level 1: Formal specification with a clear semantics for a problem to be solved (or a more abstract design), and a proof that the program satisfies this specification.

• Level 2: Full formal development (correctness-preserving transformation), and a proof that the problem specification transforms to the program written in the programming language.

Verification

Formal verification techniques can be used to prove the correctness of systems relative to a certain formal specification or property. The type of property to be verified determines the type of formalism to be used. For safety properties (something bad will not happen), model checking, a method of testing the different states of a system, is the most common. For properties of a more global nature, theorem proving is used.

Applications

Formal methods can be applied to a wide range of fields including computer science, engineering, and mathematics. They are also used in the development of high-integrity systems such as avionics software, medical software, nuclear control systems, and railway signaling.

See also

• Automata theory
• Formal language
• Formal semantics (computer science)
• Formal specification
• Model checking
• Theorem proving
• Type system

This computer science related article is a stub. You can help WikiMD by expanding it.