Motivation for the use of Formal Methods

Providing high integrity systems with embedded software requires a careful argument for its justification. Demonstrating such exacting requirements through sufficient statistical evidence based on testing and other general reliability measures has been shown to be doubtful. Thus, some other kinds of arguments have to be written, which must be precise -- in language that is well-defined, whose meaning is clear, and with the ability to prove statements without doubt. Since natural language is unable to fulfil such demands, the only possible solution is to use an approach that offers proof -- formal methods.

A formal approach is ideal for verification, the activity guaranteeing correctness, i.e. (to paraphrase) that we are building the system right and particularly that successive refinements of a specification are consistent with each other. More than that, the discipline which they encourage often leads to a more careful analysis of the most basic assumptions and definitions in the design, a benefit which is often understated. In particular, they may point to ambiguities in the requirements definition. Formal methods is thus effective for validation -- making sure that we are building the right system}.

As these formal procedures have only been applied recently, at the moment their deployment needs to be carefully targeted. The case for formal methods increases as stringency on the failure rate increases. A 'modest' failure rate may be achieved by standard software engineering, where techniques such as product testing and case analysis may suffice, whereas for stricter failure rates, such analysis is insufficient and perhaps only formal methods will do. They are particularly suited to requirements analysis where the stakes are exceedingly high in terms of the development of reliable safety-critical software.