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.

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).

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`

.

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} {} ...`

?

`b`

`X X !b`

`<> a`

`[] a`

`[] <> a`

`<> [] a`

`a U b`

`<> b -> (a U b)`

`[] (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:

`a`

`<> [] a`

`<> [] b | [] <> (!a & !b)`

`[] (a -> X !a | b)`

Assume a *finite* transition system `T`

and an LTL formula `f`

. The algorithm consists in the following steps:

- it builds an automaton
`A`

that accepts all the traces that violate`f`

- 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 - eventually, it uses classical graph algorithms (nested depth-first search, or strongly connected components decomposition) to check if
`B`

has an accepting run

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:

- Explain why this model satisfies the following two properties above
- 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`

- 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.

We consider the following imperative program:

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

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

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

What are the requirements for the protocol? Express them in LTL assuming

`AP={req1,req2,cs1,cs2}`

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

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.

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