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.


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


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)

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


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

Wednesday 8/12/99



Friday 10/12/99

Monday 13/12/99

Wednesday 15/12/99



Thursday 16/12/99

Friday 17/12/99

This is an adaptation of the page previously created by Dennis Dams, for the same OOTI SPIN workshop.
It has been maintained by Dragan Bosnacki.