OOTI SPIN Workshop (2Q215)

This page provides information about the SPIN workshop ("Workshop on Constructive Method", 2Q215) for OOTIs.

Important: The "alternative" assignment will not be accepted anymore, because three correct solutions have been submitted already!!!

The three brave men that solved the problem are (in order of appearance): Sander Kooijmans, Biao Xu, and Maikel Jansen. Congratulations!

Final assignment deadline: March 6, 2000 (firm) !
Take a look below under Final assignment and Report and submission deadline.

About Model Checking and Spin

Model checking is an approach to the verification of finite state programs. A program is unfolded into a transition system representing its state space, on which properties expressed in some form of temporal logic are then automatically checked to hold.

The paradigm enjoys an increasing acceptance by industry, as is underlined by the widespread use of model checking tools. One such tool is Spin, developed by Gerard Holzmann at Bell Labs in Murray Hill, NJ. Look here for more information on the tool.

For faster access, use this local copy of the tool documentation.

This course is centered around the Spin tool. Several concepts and methods in the area of model checking are introduced and exemplified with the help of concrete examples. Subjects to be covered are listed here. The goals of the course are listed here.

Preparation

In order to be able to use Spin, make sure you have the following directories included in your search path:

/home/titools /home/titools/bin

If your shell is csh or tcsh you can do this by inserting in your .login file the following line:

setenv PATH ${PATH}:/usr/titools:/usr/titools/bin

Please make sure that the path is set (you may have to do a rehash) and check whether it works by typing

xspin

The XSpin window should now appear on your screen. (If this is not the case, then apparently the xspin command can still not be found.)
Now Click the "Check Syntax" button. In the lower (black) part of the window, spin should now show a complaint - something like:

spin -a pan_in
spin: line 2 "pan_in", Error: syntax error
spin: line 2 "pan_in", Error: no runable process

(If this is not the case, then apparently the spin command can still not be found.) Terminate XSpin by choosing "Quit" in the "File..." menu.

If you get something like

ld.so: libX11.so.4: not found

then you need to do

setenv LD_LIBRARY_PATH /usr/X11R6/lib

export LD_LIBRARY_PATH=/usr/X11R6/lib

You might have to change the DISPLAY variable in case you're running Spin on a different machine.

Practical Information

Dates and locations:
Tuesday 7/12/99, 9.00-12.30 - HG 8.63 (SUN zaal)
Wednesday 8/12/99, 9.00-12.30 and 13.30-17.00 - HG 6.1 (WIN zaal)
Friday 10/12/99, 9.00-12.30 - HG 8.63 (SUN zaal)

Monday 13/1/99, 9.00-12.30 - HG 8.63 (SUN zaal)
Wednesday 15/12/99, 9.00-12.30 and 13.30-17.00 - HG 6.1 (WIN zaal)
Thursday 16/12/99, 9.00-12.30 - HG 8.63 (SUN zaal)
Friday 17/12/99, 9.00-12.30 - HG 8.63 (SUN zaal)

Instructor:
Dragan Bosnacki
Email: dragan@win.tue.nl
Phone: +31 40 247 5159 / 5155 (secretary)

Evaluation

Your mark will be based on the first two assignments (together 25%), the final assignment (50%) and an oral examination (25%). During the examination, the final assignment will be discussed as well as a number of topics that were presented during the lectures (material: your own notes, the papers that were handed out, and the on-line documentation, both in the tool and on the web).

Topics and Schedule

Beisdes the lectures, number of exercises will be made in hands-on sessions. The (tentative) schedule is as follows. During the course, specific material will be made available in this section.

The course has been given as developed and thought by Dennis Dams in the past two years, and earlier by Rob Gerth. The written materials that are on this page are mostly from the book Design and Validation of Computer Protocols by Gerard Holzmann, denoted in the sequel as [Hol91], and the lecture notes Concepts, Algorithms, and Tools for Model Checking by Joost-Pieter Katoen, [Kat99] in what follows. You might want also to take a look at the more general Protocol Validation course that is given by Joost-Pieter Katoen.

Tuesday 7/12/99

About the course / rules of the game.
Formal Methods, Model Checking, Spin (reading: [Kat99] System Validation, A Quick Introduction to Spin)
A quick start with Spin: a Mutual Exclusion Protocol and The Pathfinder .

Wednesday 8/12/99

morning:

Study on-line documentation.
Excercises: Disjkstra (Dekker)'s Mutual Exclusion Protocol, Mutex4a to Peterson
Another example: A Simple Communication Protocol.
Exercise: variation on the Communication Protocol.

afternoon:

Linear Temporal Logic (reading: [Kat99] Linear Temproal Logic)

Leader Election Protocol (LEP) (hands-on session)

Checking more complex properties of the LEP.

Friday 10/12/99

Assignment 1 (Peterson's Leader Election Protocol)

Monday 13/12/99

Discussion about Assignment 1. Code of one possible solution of the assignment. Version of LEP with inlines.

Fairness. Examples: Weak Fairness; Strong Fairness.
Excercise: PAR Protocol.

Wednesday 15/12/99

morning:

PAR Protocol (continued)
State-space reduction techniques (atomic, d_step, Partial order reduction, xr and xs, Minimized automaton, Bit state hashing)
Abstractions (red-white-blue, sources and sinks, etc.)

afternoon: