Basic SPIN Tutorial
Presented by Theo Ruys
April 11, 2002, morning
SPIN is a model checker for the verification of software systems.
During the last decade, SPIN has been successfully applied to trace
logical design errors in distributed systems, such as operating
systems, data communications protocols, switching systems,
concurrent algorithms, railway signaling protocols, etc.
SPIN checks the logical consistency of a specification; it reports on
deadlocks, unspecified receptions, flags incompleteness, race
conditions, and unwarranted assumptions about the relative speeds
of processes. SPIN is considered to be one of the most powerful
and advanced model checkers (freely) available today. SPIN is
widely distributed and has a large user base.
SPIN uses a high level language called PROMELA (PROcess MEta LAnguage)
to specify systems descriptions. The purpose of this tutorial is to
introduce novice users to both PROMELA and SPIN.
The first part of the tutorial (Basic SPIN) gives an introduction to
PROMELA and presents an overview of the validation and verification
features of SPIN. The material will be illustrated by several demo's
using XSpin, the graphical user interface to SPIN.
The second part of the tutorial (Advanced SPIN) discusses guidelines
to construct efficient PROMELA models and shows how to use SPIN in
the most effective way. Topics to be discussed include: SPIN's
optimisation algorithms, directives and options to tune SPIN,
aggressive PROMELA modelling, using SPIN as a debugger,
validation management and rules of thumb.
The SPIN Tutorial is targeted towards novice users of SPIN.
The second part of the tutorial, however, could also be of
considerable interest to intermediate SPIN users.