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.