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:

	web spinroot.com

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

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 2009)
  • CS119a Reliable Software: Testing and Monitoring (2008)
  • CS119b Reliable Software: Testing and Monitoring (2008)
  • CS116 Software Analysis (fall 2008)

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.

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.

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

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

• A database of Spin models maintained by Alberto Lafuente.

• A related toolset Goal: a graphical interactive tool for defining and manipulating B€chi automata and temporal logic formulae.

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.

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)
  

  For a broader overview of conversion algorithms, see: http://spot.lip6.fr/wiki/LtlTranslationAlgorithms

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

• The method for the use of embedded C code in Spin verification models (new in Spin Version 4):

    Logic Verification of ANSI-C Code with Spin,
    by G.J. Holzmann,
    Proc. SPIN2000, Springer Verlag, LNCS 1885, pp. 131-147.
    (PDF)
  
  and the abstraction method it supports is described in
  
    Model-Driven Software Verification,
    by G.J. Holzmann and R. Joshi, 
    Proc. SPIN2004, Springer Verlag, LNCS 2989, pp. 77-92.
    (PDF)
  

• The algorithms for the extension to multi-core model checking (new in Spin Version 5) are described in:

    The Design of a multi-core extension of the Spin Model Checker ,
    by G.J. Holzmann and D. Bosnacki,
    IEEE Trans. on Software Engineering, Vol. 33, No. 10, pp. 659-674.
    (PDF)
  

NewsLetters

• The Spin News Letters were originally the primary method for giving updates on changes, extensions, and revisions of the Spin sources.
  By last count, users from roughly 50 different countries were subscribed to the Newsletters.

  In the last few years, with the increased amount of spam email that we all receive, the newsletters are discontinued
  and we rely more on these online pages for announcements.
  You can always send requests for changes and extensions of the Spin software, questions on usage, and general observations to:

  spin_list [atsign] spinroot.com.

Annual Workshop

• The 17th Spin Workshop, SPIN2010, will be organized by Jaco van de Pol, jointly with Arend Rensink, Theo Ruys, and Michael Weber at Twente University and held end September 2010, co-located with ICGT 2010 and PDMC 2010 in Twente, The Netherlands.

• See also the Online Proceedings for all Spin workshops since 1995, as well as some statistics.