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