Theoretical Background

  • The following book describes the algorithms for on-the-fly verification, the underlying theory, the specification language and the tool options, for the current version of Spin.
       The Spin Model Checker: Primer and Reference Manual
       Addison-Wesley, ISBN 0-321-22862-6, 608 pgs, 2004.
    
    The book contains a complete set of manual pages for every language construct in Promela, and explain Spin's simulation and verification options.

  • An earlier book (Nov. 1990) describing Spin 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 (introduced 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 (introduced 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 (introduced 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)
    
  • The algorithms that are used to support swarm verification (supported through the swarm preprocessor to Spin, and Spin Version 5.2) are described in:
      Swarm Verification,
      by G.J. Holzmann, R. Joshi, A. Groce,
      Proc. ASE 2008, 23rd IEEE/ACM Int. Conf. on Automated Software Engineering,
      l'Aquila, Italy, Sept. 2008.
      (PDF)
      (an expanded journal version appears in:
       IEEE Trans. on Software Engineering, Vol. 37, No. 6, Nov/Dec 2011, pp. 845-857)
    
  • The design and implementation in Spin version 5.2.5 of a new and powerful bounded context switching algorithm is detailed in:
      Model checking with bounded context switching,
      by G.J. Holzmann and M. Florian,
      Formal Aspects of Computing Vol. 23, No. 3 (May 2011), pp. 365-389,
      DOI=10.1007/s00165-010-0160-5.
      (PDF)
    

Spin home page