Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Embedded Systems Validation 2003
Lecture 4
In this lecture we will take a look at SPIN.
Theo Ruys will give a
guest lecture on the model checker SPIN
and its modelling language PROMELA. You will have to make your hands dirty
with several SPIN exercises.
Program
8.30-9.20
Beginning SPIN
9.30-10.15
Advanced SPIN: Effective SPIN
10.15-10.45
Coffee break
10.45-12.00
Exercises 1 & 2 (PC-lab)
12.00-13.00
Lunch (for all in canteen)
13.00-14.00
Advanced SPIN: Scheduling with SPIN
14.00-15.00
Exercises 3 & 4 (PC-lab)
Reading Material
The main website for SPIN is spinroot.com,
which contains a wealth of information on SPIN. Apart from precise descriptions
of both SPIN and PROMELA, the site lists most foundational papers on which
the tool is based. Furthermore, the site hosts the full papers of all
ten SPIN Workshops.
As an introduction to SPIN, the following (some what outdated) documents
are highly recommended:
A reference to all PROMELA statements and SPIN options is also available
from spinroot.com:
SPIN Online References. It is convenient to have this page open in a
webbrowser while modelling in PROMELA, as one occassionally needs to
check the exact semantics of PROMELA statements.
Very recently, a new book desbribing SPIN upto version 4.0 was published.
Apart from extensive treatment of PROMELA and SPIN, the book explains the algorithms
and optimizations used in SPIN. If you are serious about SPIN this is the book to get:
Gerard J. Holzmann.
The SPIN Model Checker (Primer and Reference Manual).
Addison Wesley, Boston, 2004.
Excercises
The PDF-document esv-spin-exercises.pdf
defines the four SPIN Exercises, that will tackled on December, 5th.