ON-THE-FLY, LTL MODEL CHECKING with SPIN

[acm_logo] 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

Other References

Courses at Caltech

Some Inspiring Applications of Spin

Flood Control 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. storm barrier
Call Processing 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. Pathstar Switch
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 (pdf). 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. Cassini Spacecraft
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 report, and the more detailed appendix). 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. Toyota Probe
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. Medical

General Description

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 can be used in four main modes:

  1. as a simulator, allowing for rapid prototyping with a random, guided, or interactive simulations
  2. as an exhaustive verifier, capable of rigorously proving the validity of user specified correctness requirements (using partial order reduction theory to optimize the search)
  3. as proof approximation system that can validate even very large system models with maximal coverage of the state space.
  4. as a driver for swarm verification (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.

[spin logo]

Tool Documentation

Documentation for Spin consists of published papers and books, documentation distributed with the Spin sources, online manual pages, and the Spin Workshop proceedings. The following list points to the online documentation.

Tool Performance

Language Extensions (new)

Eclipse Plugin

Goal and Buchi Store

Emacs

Support

Sample Spin Related Projects

Annual Workshops

[spin logo]



Spin Homepage (Page Updated: 30 July 2012)