The goal of this assignment is to use the Spin model checker to verify the correctness of a couple of systems. The problems of this project are taken from the textbook Principles of Model Checking by Christel Baier and Joost-Pieter Katoen.

For this exercise, you will get to work with the Spin model checker. The model checker can be downloaded from here:
http://spinroot.com/spin/Man/README.html

There is a tutorial available here:
http://spinroot.com/spin/Doc/SpinTutorial.pdf

The following page contains information about using LTL formulas in SPIN, which will be important for this assignment:
http://spinroot.com/spin/Man/ltl.html

The input language for SPIN is called Promela. A typical program in Promela creates a fixed number of processes which run concurrently and interact either via shared variables or via channels. As an example of a very simple Promela process, consider the code below:

 proctype counter()
{
  do
    :: (count != 0) -> count = count+1
    :: (count != 0) -> count = count-1
    :: (count == 0) -> goto done
  od
  done: skip
}

The process counter randomly increments and decrements count until the process may terminate when count==0. This is a complete Promela program with a correctness property:

  int x;
  ltl p1 { [] (x >= 0) }
  proctype pp1(){
    x = x + 1;
  }
  proctype pp2(){
    x = x - 1;
  }
  init{
    x = 0;
    run pp1();
    run pp2();
  }

The init method in the program creates two processes, pp1 and pp2, which increment and decrement x respectively. The variable x is a global variable defined at the top of the program. For illustration purposes, we have added an LTL property to this file; the operator [] is spin’s textual representation of a square (the G quantifier). As a word of caution, Spin can be very picky about parenthesis in formulas, so always err on the side of too many parenthesis. Spin will try to prove or disprove that the LTL property holds for all possible interleavings of the two processes. To get started, write the code above into a file called mytest.spin.

There are two ways to run spin: simulator or verifier generator. If you run just

spin mytest.spin

Spin will run in simulator mode, which means it will try to simulate different executions of the model to try to find assertion violations. However, simulator mode will not take into account your LTL properties; it will only identify assertion violations. If you actually want to verify your ltl property, you need to run in verifier generator mode. The first step is to run

spin -a mytest.spin

Spin will generate a custom verifier into a file named pan.c; in order to actually verify the code, you need to compile pan.c and run it.

gcc pan.c -o check
./check -a

In the case of the example above, the property does not hold for all possible executions, so the verifier will output

pan:1: assertion violated  !( !((x>=0))) (at depth 8)
pan: wrote mytest.spin.trail

followed by some statistics about the verification process. The file mytest.spin.trail contains all the information necessary to reconstruct the execution that led to the property violation, but it’s not particularly readable. If you actually want to see a counterexample trace, you can get one by running the following command:

./check -r mytest.spin.trail -v

The -r flag tells the verifier to execute the program as directed by the given trail, and the -v flag tells it to show verbose output. If you run this, the verifier will show you step by step how the different threads interacted to produce the property violation.

Note: One flag you may find useful to pass to your ./check executable is -m. If your model is big, you may get an error like

error: max search depth too small, which you can fix by giving a bigger search depth with the -m flag.

Consider an elevator system that services $N > 0$ floors numbered $0$ through $N-1$. There is an elevator door at each floor with a call-button and an indicator light that signals whether or not the elevator has been called. The system must have the following properties:

• Any door on any floor is never open when the elevator is not present
• A requested floor will be served eventually
• The elevator repeatedly returns to floor 0
• When the top floor is requested, the elevator serves it immediately and does not stop on any floor on the way up

Find a set of atomic propositions – try to minimize the number of propositions – that are needed to describe the correctness properties of the elevator system as temporal logic formulas. Write a Promela model for the elevator and verify its correctness.

(For simplicity consider N=5)

We assume $N$ processes in a ring topology, connected by unbounded queues. A process can only send messages in a clockwise manner. Initially, each process has a unique identifier ident (which is assumed to be a natural number). A process can be either active or relaying. Initially a process is active. In Peterson’s leader election algorithm (1982) each process in the ring carries out the following task:

active:
d := ident; 
do forever 
begin
  /* start phase */
  send(d);
  receive(e);
  if e = ident then announce elected; 
  if d > e then send(d) else send(e); 
  receive(f );
  if f = ident then announce elected;
  if e >= max(d,f) then d := e else goto relay; 
end
 
relay:
do forever 
begin
  receive(d);
  if d = ident then announce elected;
  send(d)
end

Model Peterson’s leader election protocol in Promela (avoiding invalid end states) and verify the following properties. In an invalid end-state error the system can terminate in a state where not all active processes are either at the end of their code (i.e., at the closing curly brace of their proctype declarations) or at a local state that is marked with and end-state label.

• There is always at most one leader.
• Eventually always a leader will be elected.
• The elected leader will be the process with the highest number.

(For simplicity consider N=5)

The deadline of this project is November 30 at 11:59pm (https://mycourses.rit.edu). Please only upload your two spin files. Make a zip from your files to make uploading the files easier.

• Read the Homework Assignment Policies for the assignment policies of the course.
• This project should be done individually.