Formal modelling of systems

A model in our settings is a transition system. The goal of the following exercises is to build models that represents the behaviors of given system, with specific verification goals in mind.

Using the dot graphviz file format to write transition systems

We will use the dot graphviz language to write our transition systems and be able to easily visualize them. Moreover, in the sequel, we will reuse these models to verify their correctness using a simple model-checker.

As an example, consider the drink vendor machine model depicted below:

drink vendor machine

Here follows a description of the transition system above in the graphviz dot language:

digraph dvm {
    idle [initial="true", labels="pay"];
    coke [labels="drink"];
    sprite [labels="drink"];
    idle -> select;
    select -> coke;
    select -> sprite;
    coke -> idle;
    sprite -> idle;
}

The file specifies a graph named dvm with four nodes: idle, select, coke and sprite, and five edges. The node select is implicitly defined. The other nodes are explicitly defined. Our model-checker accepts two optional attributes on nodes:

In the specification above, the node idle is initial and labeled {pay}. The nodes coke and sprite are labeled {drink}. The node select is not labeled (i.e. it has empty label set {}).

The dot command can build a PDF (or png, or …) representation of the graph above.

  1. copy and paste the content of the code snippet above in a file dvm.dot
  2. run the command dot -Tpdf dvm.dot -o dvm.pdf
  3. open the file dvm.pdf with your usual PDF file viewer

Another simple option is to use an editor that allows real-time visualisation. For instance, Visual Code Studio (or Codium) allows to write dot files and visualise the corresponding graph side-by-side using one of the graphviz extensions.

Extending the model of the drink vendor machine

We want to extend the model of the drink vendor machine above to take into account the number of available drinks. Update the transition system above to take into account the following specification:

A model for a C program

We consider the C function below:

int f(int x)
{
  while (x != 0) {
    if (x < -1)
      x = 0;
    x = x - 1;
  }
}
  1. Model the behaviors of the C function f above as a transition system assuming that int values range from -2 to 2. What defines a state?
  2. Does it have infinite runs? What can you conclude?

A small model for a C program

We consider the following C program where the lock is initially free, and variables old and new are 8-bytes pointers. The unspecified condition ... in the if instruction has been abstracted for simplicity and should be modelled by a non-deterministic choice.

// lock is free, old and new are 8-bytes pointers
do {
  lock();
  old = new;
  if (...) {
    unlock();
    new++;
  }
}
while (new != old);
  1. How many states has this program?
  2. Build an abstract model of the program where states only keep track of: the current instruction, the status of the lock (boolean), and whether old is equal to new (i.e. the boolean value of old == new).
  3. How many states has your model? Can you prove that the lock() instruction is never blocking from your model?

Concurrent processes

We consider the C program below which has a shared variable x and a function increment that is executed by several processes. This function first stores the value of x in a local variable y. Then, it writes y+1 into x. We assume that each assignment is an atomic instruction.

int x = 0;

void increment()
{
    int y = x;
    x = y + 1;
}
  1. What defines a state of this program with N processes?
  2. Model the behavior of this program for N=2 threads as a transition system
  3. What can you conclude regarding the final value of x?