Overview of Formal Methods - Foundation for analysis methods

Formal methods provide a foundation for specification environments leading to analysis models that are more complete, consistent, and unambiguous than those produced using conventional or object-oriented methods. The descriptive facilities of set theory and logic notation enable a software engineer to create a clear statement of facts.

The underlying concepts that govern formal methods are :
- the data invariant, a condition true throughout the execution of the system that contains a collection of data.
- the state, a representation of a system's externally observable mode of behavior, or the stored data that a system accesses and alters.
- the operation, an action that takes place in a system and reads or writes data to a state. An operation is associated with two conditions : a precondition and a postcondition.

Discrete mathematics - the notation and heuristics associated with sets and constructive specification, set operators, logic operators, and sequences - forms the basis of formal methods. Discrete mathematics is implemented in the context of formal specification languages, such as OCL and Z. These formal specification languages have both syntactic and semantic domains. The syntactic domain uses a symbology that is closely aligned with the notation of sets and predicate calculus. The semantic domain enables the language to express requirements in a concise manner.

A decision to use formal methods should consider startup costs as well as the cultural changes associated with a radically different technology. In most instances, formal methods have highest payoff for safety-critical and business-critical systems.

Where are Formal Methods applied?
Although a complete formal verification of a large complex system is impractical at this time, formal methods are applied to various aspects, or properties, of large systems. More commonly, they are applied to the detailed specification, design, and verification of critical parts of large systems such as avionics and aerospace systems, and to small, safety-critical systems such as heart monitors.