Model checking has been around for more than 20 years now, and has migrated from the purely research to the industrial arena. Nowadays, it is widely accepted that its application will enhance and complement existing validation techniques as simulation and test. I try to explain here in a non-technical manner what is "model checking".

* Notice that this is intended to be "popular" account of what is model checking (always under improvement) and thus the notions here are intensionally informal, and maybe not completely precise. If you want a more formal and precise account see for instance the wikipedia entry and references therein.

How can one be sure of the correctness of critical systems, with thousands (and sometimes, millions) of components interacting in complex manners? In some cases it is possible to build the system under consideration, for instance the real chip, or coffee machine, and then "feed" the system with sensitive data to check that it really behaves as it is supposed to. This is the principle of "testing". Such approach is widely used and extremely useful in practise, though it is clearly not possible to use it in highly critical systems were the testing data could cause damages in case of errors before real deployment.

Another solution is to simulate the behaviour of the system on a computer. Simulation does not work directly on the real system, but on a model. A model is an abstract representation of the real system, usually written using Mathematics or Logic. A model is to the real system what an architect design is to the real house. One advantage of simulation is that one does not need to build the real system in order to be applied, and it is thus usually much cheaper than testing.

Both testing and simulation are widespread in industrial applications and their used have been shown to be very useful. One drawback, however, is that it is not possible, in general, to simulate or test all the possible scenarios or behaviours of a given system. That is, those techniques are in general not exhaustive due to the high number of possible cases to be taken into account (sometimes infinite in theory), and the failure cases may be among those not tested or simulated.

Is there any other technique to complement testing and simulation? The answer is yes: formal verification, a discipline lying on the border of Mathematics, Logics and Computer Science.

In order to explain temporal logic model checking we need first to understand what "temporal logic" and "automata" are.

There are sentences that are syntactically correct but not from the semantic point of view. For instance "The big house is green" is both syntactically and semantically correct (provided the house under consideration is indeed green), while "The big house is small" is contradictory as a sentence and thus semantically incorrect.

Logic takes into account syntactically well-formed sentences and studies whether they are semantically correct. The interpretation in usually given in a particular context, called "world". In normal languages the context is given by dictionaries and the informal real-life understanding of the words. In logic, a statement (syntax) is commonly interpreted in a given semantic world. If the interpretation is "true" in the given world (e.g., the big house is indeed green) then one says that the statement is "satisfied" in the given world. A valid and usual question in logic is: Is a given statement satisfied in a given semantic world? In other words, is the statement true under the interpretation?

One might be interested to know whether something will be true in the future. For example, is it possible that "sometime in the future the big house be green?". Such kind of statements can not be expressed in a precise way in "classical logic", but in an extension of such logic.

In 1957 Arthur Prior [4] wrote an influential article proclaiming the need of a good symbolic formalism to analyse philosophical questions about time. Time expressions such as "sometime in the future", "always in the future" or "always in the past", can be expressed in the so-called "temporal logic". Though the origins of such logic (first called "tense logic") were in philosophy, its main application today is in Computer Science, and in particular in the area of formal verification, thanks to the seminal work of Amir Pnueli. Pnueli proposed in 1977 [3] to use temporal logic as a framework to specify and reason about complex programs.

Arrows are often "decorated" with "labels" representing conditions or actions. When the automaton is in a given state, it can change to another state only if the given condition on an arrow connecting both states is satisfied (or similarly, if the action takes place).

If there is an arrow from state A to state B, it means that A occurs before B. Similarly, A must occur before C if there is an arrow from B to C, and one says that B and C occur in the future of A.

As an example, let us consider an automaton modelling a simple coffee machine (see Fig. 1). Initially the machine is at state "Start" and it "waits" for a coin. If a coin is provided then the machine change state to the "Button" state where two options are possible: to press the "k" button and then go to the "Coffee" state, or to press "t" and go to the "Tea" state. After serving the corresponding drink, the machine goes to the "Glass" state and it gives a glass with the chosen drink to then go back to the "Start" state.

Model checking does not work on the real system but on a model, and the properties are usually not expressed in natural language but in a formal language. Often, one represents the system as an automaton, and the properties are written in temporal logic. We explain the method with two examples.

ALWAYS (IF Button THEN (SOMETIME-IN-THE-FUTURE (Coffee OR Tea)))

Words in uppercase are temporal logic "connectives" or "operators", and the other words represent the interaction between the machine and the user. The above expression is a "formula" of temporal logic.

How can one see that the given automaton satisfies a formula? We can explain it by using the above formula and the automaton modelling the coffee machine.

We need first to understand how the connectives ALWAYS, IF-THEN, OR and SOMETIME-IN-THE-FUTURE are interpreted in the automaton. Let us assume the current state of the automaton is the initial "Start" state. Let A and B be statements, then "ALWAYS A" means that A must be true in all the states of the automaton. "IF A THEN B" means that whenever A is true in a given state, so is B. "A OR B" means that at least one of A and B must be true in the state. Finally "SOMETIME-IN-THE-FUTURE A" means that it must exist a state in the future of the current state where A is true.

It is then possible to check that the above formula is satisfied by the automaton, since from the state "Button" (after a coin is inserted) it is possible to find a state in the future such that the actions "coffee" or "tea" are possible.

ALWAYS (IF Button THEN (Coffee AND NEXT Tea))

Here NEXT is a connective formalising the "immediately after" English expression. As for the previous example it is possible to check whether the automaton satisfies the property. In this case we can see that it is not the case, since from the state "Button" one can reach the state "Coffee" and "Tea", but from the "Coffee" state it is not possible to go immediately after to the "Tea" state. This property guarantees that the machine will never allow (for the distress of the user and happiness of the machine's owner) to get coffee and then tea by paying only once.

The above examples are rather simple and in both cases a simple eye-inspection helps to give the correct answer. In general the automaton corresponding to the system may be extremely big (of the order of millions of states) and answering to such temporal questions is far from obvious. Model checking tools can answer automatically to such questions for highly complicated systems and properties.

Figures:

Fig. 1. The automaton of a coffee machine (back to text)

References:

- E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic, In: Proceedings of the Workshop on Logics of Programs, vol. 131 of LNCS, pages 52-71. Springer-Verlag, 1981.
- Simson Garfinkel. History's worst software bugs. (If for some reason the link does not work, I keep a local copy of the article here.)
- A. Pnueli. The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science, pages 46-57, 1977.
- A.N. Prior. Time and Modality. Oxford: Clarendon Press, 1957
- J.P. Queille and J. Sifakis. A temporal logic to deal with fairness in transition systems. In: 23rd Annual Symposium Foundations of Computer Science, pages 217--225, 1982.

- E.M. Clarke, O. Grumberg and D. Peled. Model Checking. The MIT Press, 1999.

Useful Links:

- COSoDIS: Contract-Oriented Software
Development for Internet Services - http://www.ifi.uio.no/cosodis/

Contact address:

Gerardo Schneider

+47 22 85 29 71

gerardo at ifi.uio.no

http://folk.uio.no/gerardo/