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
In April 2002 the tool was awarded the prestigious
System Software Award for 2001 by the ACM.
Site and Web Search:
The Spin Book
The new book, documenting the theoretical foundation
of Spin, its search algorithms, verification options, and
with a complete language reference manual for the latest version
of Spin, is available from all online book-sellers, e.g.
For a book description, see:
Some other recommended books on logic model checking, etc:
Principles of Spin,
M. Ben-Ari, Springer Verlag, 2008.
Principles of Spin (Japanese translation), M. Ben-Ari, translated by Shin Nakajima, 2010.
Principles of concurrent and Distributed Programming
(the 2nd Edition, which is based on Spin), Ben-Ari, Addison-Wesley, 2006.
Model Checking with Spin (in Japanese), by Shin Nakajima, Publ. Kindai Kaguda Sha Co., Ltd., Tokyo, April 2008, 238 pgs.
Model Checking, Clarke, Grumberg, and Peled, MIT Press, 2000.
Principles of Model Checking, C. Baier, JP Katoen, K. Larsen, MIT Press, May 2008.
Systems and Software Verification: Model-Checking Techniques and Tools,
Berard et al, Springer Verlag, 2001.
Logic in Computer Science: Modelling and Reasoning about Systems,
Huth and Ryan, Cambridge Univ. Press, 1999.
Introduction to Automata Theory, Languages, and Computation (2nd Edition),
Hopcroft, Motwani, Ullman, Addison-Wesley, 2000.
Verification of reactive systems, Klaus Schneider, Springer-Verlag 2004.
Formale Modelle der Softwareentwicklung,
by Stephan Kleuker, 2009 (in German) Covering Spin, Uppaal, and Petri Nets.
An introduction to practical formal methods using temporal logic,
by Michael Fisher, new 2011, with sections on Spin.
Wiley Publ., ISBN 978-0-470-02788-2, 353 pgs.
D is for Digital: What a well-informed person should know about computers and communications (published October 2011).
Brian Kernighan's latest book, with a general introduction to the digital world, based on his course at Princeton University.
By the K from the K&R book that introduced the C programming language many moons ago.
This book is a superb example of how to write a general science book: even those not particularly interested
in programming or computers can read this and understand it cover to cover.
Some recommended books on general programming techniques:
Writing Solid Code,
Steve Maguire, Microsoft, 1993.
Steve McConnell, Microsoft, 1993.
The Practice of Programming,
Kernighan & Pike, Addison-Wesley, 1999.
C Programming Language (2nd Edition),
Kernighan & Ritchie, Prentice Hall, 1988.
Beautiful Code: Leading Programmers Explain How They Think (Theory in Practice (O'Reilly))
Recommended rules for safety critical coding:
Courses at Caltech
- Some online lecture material:
- CS118 Logic Model Checking (winter 2011)
- CS119a Reliable Software: Testing and Monitoring (2008)
- CS119b Reliable Software: Testing and Monitoring (2008)
- CS116 Software Analysis (fall 2010)
Three examples of inspiring applications of Spin in the last few years include
the verification of the control algorithms for the new flood control
barrier built in the late nineties near Rotterdam in the Netherlands.
The verification work was carried out by the Dutch firm CMG
(Computer Management Group) in collaboration with the Formal Methods
group at the University of Twente.
Logic verification of the call processing software for a commercial data
and phone switch, the PathStar switch that was designed and built at
Lucent Technologies. The application was based on model
extraction from the full and unmodified ANSI-C code of the implementation,
which was checked for compliance with a group of roughly 20 class-5 features
formalized in linear temporal logic (e.g., call waiting, conference calling, etc.).
A cluster of 16 CPUs was used to perform the verifications overnight, every day
for a period of several months before the switch was marketed.
Perhaps the largest application of software model checking to date.
Mission Critical Software
Selected algorithms for a number of space missions were verified with
the Spin model checker. The missions include Deep Space 1, Cassini,
the Mars Exploration Rovers, Deep Impact, etc.
For Cassini, we verified the correct working of the handoff algorithms
for the dual control CPUs (pdf).
For Deep Space 1, researchers at Ames Research Center verified some
key algorithms and reported their findings in a technical report
(pdf1 which appeared in
IEEE Transactions on Software Engineering, Volume 27, Number 8, August 2001,
and the post-mortem analysis in pdf2
which appeared at the Fifth NASA Langley Formal Methods Workshop, Virginia, June 2000).
Later, at JPL a separate verification of the software used on this mission
was also done (pdf).
For the Mars Exploration Rovers we verified the correct working of
the resource arbiter that manages the use of all motors on the rovers
More recently, for Deep Impact we verified aspects of the flash file system module
that had shown problems before the encounter with the comet took place.
The picture to the right shows the Cassini spacecraft. A rapidly expanding
domain of application.
The Toyota Investigation
The model checker Spin and its Swarm verification
front-end were used extensively in NASA's detailed investigation
of the control software of the Toyota Camry MY05. The target of the
investigation, at the reques of the NHTSA from the U.S. Department of Transportation,
and executied in collaboration with the NASA Engineering and Safety Center (NESC),
was to see if the cause for unintended acceleration events could be found in software
(see p 150 of the final
and the more detailed
No direct cause for unintended acceleration was identified in this study, though
it could also not be decisively ruled out within the scope of this study.
Several candidate theories, though, were effectively disproven.
Verification of medical device transmission protocols.
Spin was used for about ten years in the verification of international standards that are used worldwide.
This work started with the
IQPS project at Eindhoven University,
and continued at the University of Groningen, both in The Netherlands.
Standards that were influenced by the Spin verification work include
Firewire IEEE 1394.1 (used in many PCs),
and ISO/IEEE 11073-20601
for medical devices.
Some of the features that set Spin apart from
related verification systems are:
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 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 (starting with version 5) provides direct support for
the use of multi-core computers for model checking
runs -- supporting both safety and liveness verifications.
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
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
Spin can be used in four main 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.
as a driver for
(a new form of swarm computing), which can make optimal
use of large numbers of available compute cores
to leverage parallelism and search diversification techniques,
which increases the chance of locating defects in very
large verification models.
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.
Documentation for Spin consists of
published papers and books, documentation distributed with
the Spin sources, online manual pages,
and the Spin Symposia proceedings.
The following list points to the online documentation.
README.html with the downloading and installation notes for Spin.
Or follow the direct links to the latest 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.,
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
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
A Japanese translation of the Manual is also available.
- Theoretical Background
A good number of papers and books have been written about the algorithms and the
automata theoretic framework that Spin is based on.
You can find a list of the most important papers at this link.
Modifications, updates, extensions, fixes of the Spin sources
are documented in the files V.Updates, which are part of
the main Spin distribution archive. (And you can also find them
on the Binary and
Source distribution pages.) The file
Doc/V5.Updates, for instance, gives the update history for the
most recent version of Spin.
Included in the Doc directory of the Source distribution are also
files with errata to the first edition of the book,
answers to selected exercises, and all examples from that book.
More Promela examples can be found in the Test
directory from the distribution archive, and in the papers on Spin.
A short description of Spin's Roots.
A database of Spin models
maintained by Alberto Lafuente.
Recently our colleagues at Brno have assembled a valuable
of verification models, with a wealth of information.
Included in the database are models in DVE format with some performance
data, and available are also mechanically generated versions in Promela
of the same models.
We have added performance numbers for Spin for all models in this database
that have a Promela version (about 232 models or model variants).
The results are tabulated on this summary page.
(Most of the performance data tabulated on this page is machine generated from scripts.
Please send a note if you spot any inaccuracies.)
The Minnesota Extensible Language Tools group (MELT), and specifically
Eric Van Wyk
(evw [atsign] cs.umn.edu) has made some very interesting
extensions to the Promela language available via an online translation tool on
the web. As their webpage says:
"These extensible language frameworks are all constructed using the extensible language tools
developed by the MELT group. The distinguishing characteristic of our approach to extensible
languages is that the extensions can be easily composed, even if they are developed
by different parties."
The translation tool allows you to convert extended Promela specifications into pure Promela.
The extensions currently supported include:
- A non-deterministic choose construct that evaluates to a random value in a specified range.
- A multi-dimensional array construct that allows one to declare variables to be arrays of more than one dimension.
(Promela itself only supports single dimension arrays directly.)
- A condition-table construct that is borrowed from synchronous modelling languages like RSML or SCR.
The link to the conversion server, with a number of example extended Promela models
that can be converted online, is:
The source code for the extension itself will soon also be available for downloading from
the same webpage.
The new Eclipse plugin, described at the 2009 Spin Symposium by
Tim Kovse and colleagues from the University of Maribor in Slovenia,
is available from:
together with the installation and usage instructions. It offers a
very nice folding editor for Promela models.
An extension for displaying Spin error trails as message sequence charts can be
downloaded from: http://lms.uni-mb.si/st2msc/.
More extensions are planned, providing more of the functionality of
the current Xspin interface.
Büchi Store is a repository
of Büchi automata and their complements for common specification
patterns and interesting temporal formulae.
The three smallest automata known are included.
Users can upload new automata or smaller equivalent ones.
The repository can be useful as benchmark cases for researching
Büchi complementation algorithms and as examples for teaching.
Goal is a toolset closely
related to Spin. It is a graphical interactive tool for defining
and manipulating Büchi automata and temporal logic formulae.
- There are several versions of a Promela mode for
A quick Google search for "Promela emacs" will find them, or try:
Spin is actively maintained and continuously improved and updated.
If you send in a bug report, you'll typically
get a response in minutes, and confirmed bugs are normally fixed within a few days
at the most.
Feel free to send requests for changes and extensions of the Spin software,
questions on usage, bug reports, and general observations to:
spin_list [atsign] spinroot [dot] com.
Click here for a list of currently open issues
that can be considered for everything
from a summer project to a longer term research project.
The topics are divided into three categories, depending on the
expected level of difficulty: Basic, Intermediate, and Advanced.
Charter for the Spin Symposia series, and steering committee.
Online Proceedings for all 19 Spin Symposia held since 1995 (initially as Workshops).
The Spin 2013 Symposium (#20) will be held at Stony Brook University, in New York
on 8 and 9 July 2013, chaired by Scott Smolka, Ezio Bartocci, and C.R. Ramakrishnan.
Abstract submission deadline: 8 March 2013. Full papers: 15 March 2013. Final versions: 24 April 2013.
We're inviting proposals for organizing Spin 2014 and beyond,
if you're interested in organizing a Spin Symposium, please send a note to one of the Spin SC members.