This page provides information about the SPIN workshop ("Workshop
on Constructive Method", 2Q215) for OOTIs.
Final assignment deadline: March 6, 2000 (firm)
!
Take a look below
under Final assignment and Report
and submission deadline.
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.
/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
or
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.
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)
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
morning:
Friday 10/12/99
Monday 13/12/99
Wednesday 15/12/99
morning:
Thursday 16/12/99