`ON-THE-FLY, LTL MODEL CHECKING with SPIN`

Spin is a popular open-source software tool, used by thousands of people worldwide, that can be used for the formal verification of distributed software systems. The tool was developed at Bell Labs in the original Unix group of the Computing Sciences Research Center, starting in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field. In April 2002 the tool was awarded the prestigious System Software Award for 2001 by the ACM.

`Quick Links`

`Site and Web Search:`

`The Spin Book`

http://spinroot/spin/Doc/Book_extras/index.html

click: Model Checking, Clarke, Grumberg, and Peled, MIT Press, 2000.
click: Systems and Software Verification: Model-Checking Techniques and Tools, Berard et al, Springer Verlag, 2001.
click: Logic in Computer Science: Modelling and Reasoning about Systems, Huth and Ryan, Cambridge Univ. Press, 1999.
click: Introduction to Automata Theory, Languages, and Computation (2nd Edition), Hopcroft, Motwani, Ullman, Addison-Wesley, 2000.

Some recommended books on general programming techniques:

click: Writing Solid Code, Steve Maguire, Microsoft, 1993.
click: Code Complete, Steve McConnell, Microsoft, 1993.
click: The Practice of Programming, Kernighan & Pike, Addison-Wesley, 1999.
click: C Programming Language (2nd Edition), Kernighan & Ritchie, Prentice Hall, 1988.

`General Description`

Some of the features that set Spin apart from related verification systems are:

Spin targets efficient software verification, not hardware verification. The tool supports a high level language to specify systems descriptions, called PROMELA (a PROcess MEta LAnguage). Spin has been used to trace logical design errors in distributed systems design, such as operating systems, data communications protocols, switching systems, concurrent algorithms, railway signaling protocols, etc. The tool 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 (starting with version 4) provides direct support for the use of embedded C code as part of model specifications. This makes it possible to directly verify implementation level software specifications, using Spin as a driver and as a logic engine to verify high level temporal properties.
Spin works on-the-fly, which means that it avoids the need to preconstruct a global state graph, or Kripke structure, as a prerequisite for the verification of system properties.
Spin can be used as a full LTL model checking system, supporting all correctness requirements expressible in linear time temporal logic, but it can also be used as an efficient on-the-fly verifier for more basic safety and liveness properties. Many of the latter properties can be expressed, and verified, without the use of LTL.
Correctness properties can be specified as system or process invariants (using assertions), as linear temporal logic requirements (LTL), as formal Büchi Automata, or more broadly as general omega-regular properties in the syntax of never claims.
The tool supports dynamically growing and shrinking numbers of processes, using a rubber state vector technique.
The tool supports both rendezvous and buffered message passing, and communication through shared memory. Mixed systems, using both synchronous and asynchronous communications, are also supported. Message channel identifiers for both rendezvous and buffered channels, can be passed from one process to another in messages.
The tool supports random, interactive and guided simulation, and both exhaustive and partial proof techniques, based on either depth-first or breadth-first search. The tool is specifically designed to scale well, and to handle even very large problem sizes efficiently.
To optimize the verification runs, the tool exploits efficient partial order reduction techniques, and (optionally) BDD-like storage techniques.

To verify a design, a formal model is built using PROMELA, Spin's input language. PROMELA is a non-deterministic language, loosely based on Dijkstra's guarded command language notation and borrowing the notation for I/O operations from Hoare's CSP language.

Spin can be used in three basic modes:

as a simulator, allowing for rapid prototyping with a random, guided, or interactive simulations
as an exhaustive verifier, capable of rigorously proving the validity of user specified correctness requirements (using partial order reduction theory to optimize the search)
as proof approximation system that can validate even very large system models with maximal coverage of the state space.

All Spin software is written in ANSI standard C, and is portable across all versions of Unix, Linux, cygwin, Plan9, Inferno, Solaris, Mac, and Windows.

[spin logo]

`Tool Documentation`

Documentation for Spin consists of published papers and books, documentation distributed with the Spin sources, online manual pages, the Spin Newsletters, and the Spin Workshop proceedings. The following list points to the online documentation. The most important papers and books can be found in the next section.

README.html with the downloading and installation notes for Spin.
ONLINE REFERENCES, including a semantics definition for the specification language Promela, and manual pages explaining the run-time options for Spin and for the verifiers generated by Spin. You can optionally also download a local copy of the manpages from the archives, e.g., pc_man.zip, or html.tar.gz, but be warned that these get outdated, while the online references are more likely to be up to date.
If you have installed both Spin and Xspin, and want to learn how to use Xspin, then read GettingStarted If you want to learn how to use Spin directly from the command-line, then read Roadmap and Exercises For more detailed information, read also Manual and then WhatsNew.html
Modifications, updates, extensions, fixes of the Spin sources are documented in the files V[1234].Updates, which are part of the main Spin distribution archive. In directory Doc, the file Doc/V4.Updates for instance, gives the update history for the most recent version of Spin.
Included in the Doc directory are also files with errata to the first edition of the book, answers to selected exercises, and all examples. More Promela examples can also be found in the Test directory from the distribution archive, and in the papers on Spin.
A short description of Spin's Roots.

`Theoretical Background`

A new book (Sept. 2003) describes the algorithms, including the on-the-fly verification algorithms, the underlying theory, the language and all tool options, for the most recent version of Spin (version 4) is now available at all online book sellers.
```
   The Spin Model Checker: Primer and Reference Manual
   Addison-Wesley, ISBN 0-321-22862-6, 608 pgs, cloth-bound.
```
The book contains a complete set of manual pages for every language construct in Promela, and explain every Spin verification option.

The first book (now outdated) describing Spin (Nov. 1990) was:

   Design and Validation of Computer Protocols,
   Prentice Hall, New Jersey, 1991, ISBN 0-13-539925-4.
   A paperback edition of the book is still available from
   www.amazon.com.
   There is also a Japanese translation of the book.

An overview paper of Spin, with verification examples, is:

   The Model Checker Spin,
   IEEE Trans. on Software Engineering,
   Vol. 23, No. 5, May 1997, pp. 279-295.
   (PDF)

The automata-theoretic foundation for Spin:

   An automata-theoretic approach to automatic
   program verification,
   by Moshe Y. Vardi, and Pierre Wolper,
   Proc. First IEEE Symp. on Logic in Computer Science,
   1986, pp. 322-331.
   (PDF)

The algorithm for bitstate hashing (optional in Spin for verifying large problem sizes) is discussed in detail in:

   An analysis of bitstate hashing,
   by G.J. Holzmann, Formal Methods in Systems Design, Nov. 1998
   (PDF)

The algorithm for partial order reduction is described in:

   An Improvement in Formal Verification,
   by G.J. Holzmann and D. Peled,
   Proc. FORTE 1994 Conference, Bern, Switzerland.
   (PDF)

The nested depth first search algorithm used in Spin:

   On nested depth-first search,
   by G.J. Holzmann, D. Peled, and M. Yannakakis,
   in The Spin Verification System, pp. 23-32,
   American Mathematical Society, 1996. (Proc. of the 2nd Spin Workshop.)
   (PDF)

Wolper's hash-compact method (optional in Spin version 3.2.1 and later) was first presented and analyzed in:

   Reliable hashing without collision detection,
   by Pierre Wolper and Dennis Leroy,
   Proc. 5th Int. Conference on Computer Aided Verification, 1993,
   Elounda, Greece, pp. 59-70.
   (PDF)

The algorithm for conversion of LTL to Buchi Automata (in Spin terminology: never claims) is described in:

   Simple on-the-fly automatic verification of
   linear temporal logic,
   by Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper,
   Proc. PSTV 1995 Conference, Warsaw, Poland.
   (PDF)

The algorithm for storing reachable states with a minimized automaton (new in Spin Version 3)

   A Minimized automaton representation of reachable states,
   by A. Puri and G.J. Holzmann,
   Software Tools for Technology Transfer, Vol. 3, No. 1, Springer Verlag.
   (PDF)

`NewsLetters`

The Spin News Letters give updates on all changes, extensions, and revisions of the sources since the book was published. You can subscribe to the email distribution of these newsletters by sending a one-line message Subscribe to spin_list@spinroot.com
New releases of the Spin software are announced through these newsletters. Occassionally the newsletters also include answers to frequently asked questions, describe main new applications or projects with Spin. The newsletter serves mainly to establish contacts between people using the Spin software in different countries (there are users in over 40 different countries).
Anyone who wants to announce an extension of the basic Spin software, to seek advice from or contacts with other Spin users, to make available postscript versions of papers on Spin usage (e.g. by anonymous ftp or as a URL on the internet) for feedback or communication, can also submit such items for inclusion in announcements to the mailing list.

`Annual Workshops`

The next, 12th, Spin workshop

SPIN2005

will be organized by Patrice Godefroid and co-located with CONCUR 2005.
The SPIN workshop will be held August 22-24 (3 days) 2005 and CONCUR will be held
August 23-26, 2005, both at the Stanford Court Hotel in San Fransisco, California.
(The last two days of SPIN2005 overlap with CONCUR2005.)

Online proceedings for all previous workshops can be found in:

spin_list [at] spinroot.com (Page Updated: 19 October 2004)