What are Formal Methods?

Formal methods may be defined as a branch of discrete mathematics which deals with the logical analysis of forms and their semantics (meaning), with a specific application domain being computing. They usually consist of two parts:

  1. a formal calculus (or formal system) which is a symbolic system in which are defined axioms, having some denotation as formulae; a precise syntax that defines how the axioms may be put together; and relations that enable the deduction of properties purely as the conclusion of arguments that are valid through the system's syntax.
  2. a formal language is a formal calculus which has also an interpretation of the formulae -- semantics. Further rules constrain what constitute valid (meaningful) formulae and the properties that may be deduced. A given calculus may have infinitely many interpretations.
The fruits of the first part are propositions and theorems which express properties about the formulae. The second part generates the same kind of results, but also allows reasoning within given contexts. The mathematical disciplines used are based on set theory, predicate logic and algebra; the 'methods' in formal methods are techniques related to these disciplines.

At first sight this may appear off-putting to an engineer who is unfamiliar with this kind of maths. It is rather a contrast with the usual conotation of 'methods' in industry, which are procedures to generate working products. As many authors have pointed out, the general lack of such an industrial view, has proved a great stumbling block.

However, the second part allows the more liberal view that formal methods may be regarded as a mathematical approach to {reason about} any system, be it an industrial factory or an abstract machine. It is just another language to make ourselves clearly understood by others and continue development in a sure-footed manner. Further, there are efforts to integrate the formal approach into working methodologies that are recognised by industry.

Why Formal Methods are useful | Index to Formal Methods

- Paul Trafford Paul's home page

Page created: 27 May 1998