In computer science, formal methods refers to mathematically based techniques for the specification, development and verification of software and hardware systems (Foldoc:formalmethods).

The role of formal methods in software engineering engenders much controversy.

Taxonomy

As with the sub-discipline of programming language semantics, formal methods may be roughly classified as follows:

• Denotational semantics, in which the meaning of a system is expressed as a mathematical function. Proponents of such methods rely on the well-understood nature of functions to give meaning to the system; critics point out that not every system may be intuitively viewed as a function.
• Operational semantics, in which the meaning of a system is expressed as a sequence of actions of a (presumably) simpler computational model. Proponents of such methods point to the simplicity of their models as a means to expressive clarity; critics counter that the problem of semantics has just been delayed (who defines the semantics of the simpler model?).
• Axiomatic semantics, in which the meaning of the system is expressed in terms of preconditions and postconditions which are true before and after the system performs a task, respectively. Proponents note the connection to classical logic; critics note that such semantics never really describe what a system does (merely what is true before and afterwards).

Uses

Formal methods can be applied at various points through the development process. (For convenience, we use terms common to the waterfall model, though any development process could be used.)

Specification

Formal methods may be used to give a description of the system to be developed, at whatever level(s) of detail desired. This formal description can be used to guide further development activities (see following sections); additionally, it can be used to verify that the requirements for the system being developed have been completely and accurately specified.

The need for formal specification systems has been noted for years. In the ALGOL 60 Report, John Backus presented a formal notation for describing programming language syntax (later named Backus normal form (BNF)); Backus also described the need for a notation for describing programming language syntax. The report promised that a new notation, as definitive as BNF, would appear in the near future; it never appeared.

Development

Once a formal specification has been developed, the specification may be used as a guide while the concrete system is developed (i.e. realized in software and/or hardware). Examples:

• If the formal specification is in an operational semantics, the observed behavior of the concrete system can be compared with the behavior of the specification (which itself should be executable or simulateable). Additionally, the operational commands of the specification may be ameneable to direct translation into executable code.
• If the formal specification is in an axiomatic semantics, the preconditions and postconditions of the specification may become assertions in the executable code.

Verification

Once a formal specification has been developed, the specification may be used as the basis for proving properties of the specification (and hopefully by inference the developed system).

• Human-directed
• Automated

Criticisms

There is extensive debate about the effectiveness of formal methods. Proponents argue that this approach does not require conventional coding any more. Detractors point out that proofs of correctness tend to be 10 times larger than the programs, which makes them unrealistic. Very few specifications exist that are precise enough for formal methods to apply. And, very few examples exist where formal methods were used.

There have been a variety of successes with formal methods, such as weakest preconditions . When originally proposed, programmers were to use weakest preconditions to prove that loops halt. In practice, most loops are too obvious to need a proof, so such a proof would be useless. However, weakest preconditions are very useful for guiding compiler optimization. So, formal methods are used when optimizing every single loop in a program.

This is a common pattern: a formal method is proposed for humans to prove that their code works properly. But, the technique is most useful when it can be systematically or automatically applied to all code. This means that it needs to be applied by a compiler, because humans are not good at consistency. So, all useful formal methods eventually become part of the compiler. Humans continue to develop the remaining high-level issues.

Example

Thowa 10:42, 17 Apr 2005 (UTC): None of the formal methods can be shortly explained within a Wiki-discussion. But let's do a short example, a more interested reader might find as a useful starting point to understand how powerful formal methods in practise are.

Let's create a finite state machine (FSM) having two states "Eat" and "Sleep". This FSM shall communicate with two external objects: a digital input (di) and a timer (ti). The digital input can generate two signals: “true” and “false”. The timer generates one signal “over”. The timer accepts also a command “start” (which does a reset and starts the timer). We create an input and output dictionary which can be used by the FSM:

Input dictionary

{di_true, di_false, ti_over}

Output dictionary

{ti_start}

What does our example FSM do? It starts in state “Eat” and goes to state “Sleep” in case the di was set to “true”. Entering the state “Sleep” the FSM starts the timer. To go back to state “Eat” the timer must be “over” (ti_over) and the di must be changed to “false” (di_false). Please print the FSM transition diagram on a piece of paper to avoid any misunderstanding. To create the executable specification we need to create state transition tables for each state of our FSM:

and

An automatic process can generate a set of equations which fully express the above specification. This set could look like this (note that this is already a kind of machine code, so it looks criptical, but I enter it here to show the “magic” behind the executable specification):

S1 N2 V4 S2 E1 N1 V3&2

where S represents the current state, N the next state, E entry action and V condition (& means AND). For instance the first line means “in state 1 (Eat) go to state 2 (Sleep) if the boolean condition 4 (di_true) is true”.

Some words about the used boolean algebra here. In the presented concept it is the positive logic algebra and not the boolean algebra (i.e. NOT is forbidden). The reason is simple: in the software world we have very seldom signals which can be negated. Lets take for instance a sensor which delivers temperature: temp_low, temp_good and temp_high. What would be NOT temp_high? So in the above concept we only look if a signal exists or not. Some signals cannot exists in parallel, e.g. We cannot have at the same time di_true and di_false.

The above equation plus the description of the I/O dictionaries can be now read by a standard executor (which might be a part of the OS) and executed.

Related Topics

• automated theorem proving
• model checking

References

• Formal methods publications

External links

• Virtual Library formal methods
• Z notation