Formal design of software with a model-checker

We study model-checking as a technique to design reliable software. Model-checking consists in checking that a mathematical model of the software is correct with respect to a formal specification. The model can then be used as a basis for code production, either automatically or manually, as well as to generate test cases to assert the correctness of the software.

Configuration of the model-checker

We will use a simple model-checker to illustrate the concepts introduced in this class. The tool is already installed at ENSEIRB-MATMECA under the following path: ~herbrete/public/simple-ltl-model-checker/model-checker.py. In order to use it:

• please connect on a machine with all the requires softwares installed, for instance: lsd, cocaine, …
• and add the following path /net/ens/herbrete/public/linux/lib64/python3.6/site-packages to your PYTHONPATH environment variable.

Simply run ~herbrete/public/simple-ltl-model-checker/model-checker.py -h to check that your configuration is well set up. It should display the following message:

usage: model-checker.py [-h] [--output OUTPUT] model formula

positional arguments:
  model            model file name
  formula          LTL formula to check

optional arguments:
  -h, --help       show this help message and exit
  --output OUTPUT  output kripke structure, automaton and product using OUTPUT
                   as a file name prefix

Please refer to the webpage for the documentation of the tool. Usage information is obtained using option -h (as above).

Model-checking

System model: transition systems

We are interested in proving the correctness of a system (or to show that it is incorrect when it is the case). The correctness of a software relies on its executions that should all satisfy the specification. Hence, in our setting, a model of a software is the set of its behaviors.

A behavior represents the evolution of a software during its execution. The software starts in an initial state (for instance, the server is waiting for a request), then it evolves to the next state when an event occurs (for instance, when a request is received, or when the answer is sent), and so on. Hence, we basically need to represent the state space of the software, as well as the evolution from each state to the next states. It is thus very convenient to represent the behaviors of a system as a graph, which we call a transition system since it has distinguished initial states (which graphs usually do not have). Formally, a transition system T=(S,S0,->,AP,L) is defined by:

• a set S of states with initial states S0,
• a transition relation -> that links a state to its successor states,
• a set AP (for atomic propositions) of labels, and a state labeling function L that associates a set of labels from AP to every state in S.

The picture below depicts a transition system:

In this class we will only consider finite-state systems as it will be required to ensure termination of model-checking algorithms.

A run is any sequence of states starting from an initial state, and following transitions. For instance: s0 -> s1 -> s0 -> s1 is a run. However s1 -> s2 is not run as it does not start from an initial state. Similarly, s2 -> s1 is not a run as there is no transition from s2 to s1.

A trace is the sequence of labels of the states on a run. For instance: {a} {} {a} {} {a} {} is the trace of the run s0 -> s1 -> s0 -> s1 -> s0 -> s1.

Property specification: Linear Temporal Logic (LTL)

We have just seen how systems are modelled as transition systems. A transition systems describes a (potentially infinite) set of behaviors (or runs), that we observe as traces. The goal of the specification is to define the set of valid traces independently from the model. Then, a model-checker can be used to assert that all the traces of the model are valid with respect to the specification.

From now on, we only consider infinite traces. We introduce the Linear Temporal Logic (LTL) as a way to describe sets of infinite traces. Assume a set AP of atomic propositions. The LTL formulas over AP are defined by:

• a is a formula, for any atomic propositions a from AP
• if f and g are two LTL formulas, then !f (not), f & g (and), f | g (or), f -> g (implies), X f (next), f U g (until), [] f (always) and <> f (eventually) are LTL formulas.

Assuming AP={a,b,c}, a is an LTL formula, a & b is also an LTL formula, a U (b & c) is an LTL formula, and [] (a -> X b) is also an LTL formula.

We will now give a meaning to these formulas. Consider an infinite sequence l of sets of atomic propositions: l = l1 l2 l3 ... where each li is a subset of AP. We have:

• l |= a if l1 contains a. That is: a sequence l satisfies the atomic proposition a if a is among of the first labels of l
• l |= f & g if l |= f and l |= g. That is a sequence satisfies the formula f & g iff it satisfies both f and g (and similarly for the other boolean operators !, |, -> according to their usual semantics)
• l |= X f if l2 l3 ... |= f. That is: l satisfies X f if f holds from the second position in l
• l |= [] f if every suffix of l satisfies f: li ... |= f for every i >= 1. That is: l satisfies [] f is f holds from every position in l, or in other words, if f is always true
• l |= <> f if f is true in some suffix of l: there exists i >= 1 such that li ... |= f. In other word, l satisfies <> f if f eventually holds on l
• l |= f U g if g is true in some suffix of l, and f is true in the meantime: there exists i >= 1 such that li ... |= g and for all 1 <= i < j, li ... |= f. That is, l satisfies f U g if g is eventually true, and f is always true before g becomes true.

Which ones of the properties below are satisfied by the trace: {a} {} {a} {} {a} {} {a} {} ...?

1. b
2. X X !b
3. <> a
4. [] a
5. [] <> a
6. <> [] a
7. a U b
8. <> b -> (a U b)
9. [] (a -> X !a)

A transition system T satisfies an LTL formula f, denoted T |= f, if every trace l of T satisfies f, that is l |= f.

Tell which if the following properties below are satisfied by the following transition system:

1. a
2. <> [] a
3. <> [] b | [] <> (!a & !b)
4. [] (a -> X !a | b)

The model-checking algorithm

Assume a finite transition system T and an LTL formula f. The algorithm consists in the following steps:

1. it builds an automaton A that accepts all the traces that violate f
2. then it computes the product of T and A. The resulting automaton B accepts all the runs of T that violates f. Hence, T satisfies f if and only if B has no accepting run
3. eventually, it uses classical graph algorithms (nested depth-first search, or strongly connected components decomposition) to check if B has an accepting run

A first example: the drink vendor machine

We want to program a drink vendor machine that ensures the following two properties:

• the consumer cannot get a drink without paying first
• every drink paid by the consumer is delivered to her

We propose the model below:

1. Explain why this model satisfies the following two properties above
2. Express the requirements above in LTL, and check that the model of the drink vendor machine satisfies the requirements using the python script model-checker.py
3. Refine the model to check that the consumer pays 2 euros before the drink is delivered. Coins of 0.5, 1 and 2 euros can be used to pay the drinks. Check that your new model satisfies the requirements using the model-checker.

A second example: a small program

We consider the following imperative program:

// PRECOND: -2 <= x <= 2
while (x != 0) {
  if (x < -1)
    x = 0;
  x = x - 1;
}
// POSTCOND: x == -1

1. Draw the transition system corresponding to this algorithm. Does it have finite runs? Infinite runs?
2. Check that the post-condition hold upon termination using the model-checker. Explain what you observe.
3. How can we check termination of the algorithm?

A third example: mutual exclusion

Our goal is to design a mutual exclusion protocol to prevent a system of two processes to access a critical resource simultaneously.

1. What are the requirements for the protocol? Express them in LTL assuming AP={req1,req2,cs1,cs2}.

2. Check the model against your specification using the model-checker. Explain the result.

3. Fix the model using a lock to prevent the two processes to access the critical section simultaneously. Check the bew model against the specification using the model-checker. Explain the result.

4. Use extra labels to model progress of each process. Then, check that the requirements hold under fairness conditions below:

   • unconditional fairness: each process progresses infinitely often
   • weak fairness: if access to critical section is continuously enabled, then the process is granted access infinitely often
   • strong fairness: if access to critical section is enabled infinitely often, then the process is granted access infinitely often