Formal Methods

Formal methods are mathematical approaches to software and system development which support the rigorous specification, design and verification of computer systems. The use of notations and languages with a defined mathematical meaning enable specifications, that is statements of what the proposed system should do, to be expressed with precision and no ambiguity. The properties of the specifications can be deduced with greater confidence and replayed to the customers, often uncovering facets implicit in the stated requirements which they had not realised. In this way a more complete requirements validation can take place earlier in the life-cycle, with subsequent cost savings.

Designs, likewise expressed in a language with a mathematically defined meaning, can be methodically derived from the specifications as to provably possess all their properties. Several levels of specification and/or design may be produced, each derived from and fulfilling the properties of its predecessor. This process is known as refinement or reification - to reify is to make something into `a thing’ or more concrete. The lower levels of design will typically use language structures which are closer to those found in the programming language in which the software is implemented. This final reification step can be proved correct only if the implementation language has a formally defined meaning, or semantics. This is the case with an increasing number of languages (Ada, Pascal and Modula-2 are examples) and the formal semantics definitions of some languages have now started to be incorporated in their international standard definitions. Even if the implementation language does not have a written definition of its formal semantics, one can justifiably have greater confidence in the correctness of the implementation if the step from the lowest level of design to the implementation is clear, visible and detailed.

After an initial training period, using formal methods rarely costs more than using conventional methods in a development, provided the formal method has been sensibly integrated into the organisation’s current development life-cycle. The usual experience is that costs are greater and time-scales longer during the earlier stages of the life-cycle, but are more than compensated by lower costs and shorter time-scales in the later stages of the development. There is no evidence that the resulting implementations are any less efficient in time or space; indeed, there is some empirical evidence showing the reverse.