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.

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. at amazon.com
For a book description, see: http://spinroot/spin/Doc/Book_extras/index.html.

Other References

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.


Recommended (introductory):

• 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.
• Code Complete, 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:

• The Power of Ten: rules for writing safety critical code.
• Related: An overview of static source code analyzers

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)

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.
	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.
	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.
	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.
	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.

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 (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 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.

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.

Tool Documentation

• README.html with the downloading and installation notes for Spin.
  Or follow the direct links to the latest Spin Binaries or Sources.

• 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
  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[1234].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.

Tool Performance

Recently our colleagues at Brno have assembled a valuable database 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.)

Language Extensions (new)

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:

http://www.melt.cs.umn.edu/demos/promela/index.html.

The source code for the extension itself will soon also be available for downloading from the same webpage.

Eclipse Plugin

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: http://lms.uni-mb.si/ep4s/, 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.

Goal and Buchi Store

• 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.

Emacs

• There are several versions of a Promela mode for Emacs available. A quick Google search for "Promela emacs" will find them, or try: promela-mode.el.

Support

• 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.

Sample Spin Related Projects

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.

Annual Symposia

• Charter for the Spin Symposia series, and steering committee.
• Online Proceedings for all 19 Spin Symposia held since 1995 (initially as Workshops).

• The 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.
  Final dates: 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.