Model Checking: A Complement to Test and Simulation

Author: Gerardo Schneider

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.


Our daily life dependency on computer-based applications (both hardware and software) has motivated Computer Science researchers to develop new techniques to increase our confidence on their correctness. Such applications range from simple coffee machines to nuclear plants passing by flight control towers. Many of those applications are undoubtedly critical and a failure may cause high damages, both economically and physically. Just to mention one of such big catastrophes, the 4th of June 1996, the European rocket Ariadne exploded just few seconds after launching, costing millions of dollars and many years of lost work. An enquiry found that the error could have been avoided with the use of formal methods techniques to detect the software error which caused the disgrace. (For an account of this and other "classic" software bugs, see for instance Garfinskel's article.)

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.


Formal verification comprises many different techniques, being the common denominator their basis on solid mathematical and logical foundations. In this sense, some researchers also include testing, provided it is based on formal techniqques. We describe here one technique called "temporal logic modal checking", which was introduced in the beginning of the 80's, independently by Queille and Sifakis (France) [5], and Clarke and Emerson (USA) [1].

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

Temporal Logic

In the same way as natural languages (e.g., Norwegian and English), mathematical (classical) logic has syntax and semantics. Syntax determines the rules to build well-formed words and sentences, whereas semantics provides their interpretation or meaning.
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.


An "automaton" may be defined to consist of a set of "states" and a set of "relationships" between the states. States are usually depicted as circles while relations are depicted as arrows between the states.

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.

Temporal Logic Model Checking

When one builds a system to perform a given task it is common to define a set of properties the system must satisfy. Model checking is a technique used to answer to the following question: Does the system satisfy the given properties?

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.

Example 1.

The property "Always, after the machine gets a coin and the user press a button, it gives coffee or tea", can be written in temporal logic as:


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.

Example 2.

Let us consider now the following property: "Always, after pressing a button the machine will serve coffee and then tea immediately afterwards". We can write this sentence as follows:

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.


The technique described here has been applied in a number of real-life applications, notably in hardware verification and to prove correctness of a variety of software protocols (see for instance the book on Model Checking by Clarke et al book). In the COSoDIS project in particular, we are using model checking as a verification technique for analysing (legal and electronic) contracts (see link below).


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

  1. 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.
  2. 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.)
  3. A. Pnueli. The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science, pages 46-57, 1977.
  4. A.N. Prior. Time and Modality. Oxford: Clarendon Press, 1957
  5. 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.

Useful Links:

Contact address:
Gerardo Schneider
+47 22 85 29 71
gerardo at