General Description

Some of the features that set Spin apart from related verification systems are:

  • Spin targets the efficient verification of multi-threaded software, not the verification of hardware circuits. The tool supports a high level language to specify systems descriptions called PROMELA (short for: 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, control software for spacecraft, nuclear power plants, etc. The tool checks the logical consistency of a specification and reports on deadlocks, race conditions, different types of incompleteness, and unwarranted assumptions about the relative speeds of processes.

  • Spin 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. With the help of the model extractor modex it is also possible to mechanically derive a PROMELA model from concurrent C code, and verify it with Spin.

  • Spin provides direct support for the use of multi-core computers for model checking runs - supporting the verification of both safety and liveness properties.

  • 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. This makes it possible to verify very large system models.

  • 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 Spin never claims.

  • The tool is one of very few verification tools that 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, which makes it possible (for instance) to verify models from mobile pi-calculus.

  • The tool supports random, interactive and guided simulation, and both exhaustive and partial proof techniques, based on depth-first search, breadth-first search, or bounded context-switching. The tool is designed to scale well, and to handle large problem sizes efficiently.

  • To optimize verification runs, Spin exploits efficient partial order reduction techniques, and (optionally) BDD-like state storage techniques.
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.

Main Usage Modes

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 swarm verification (a new form of swarm computing that can exploit cloud networks of arbitrary size), 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 ISO-standard C, and is portable across all versions of Unix, Linux, cygwin, Plan9, Inferno, Solaris, Mac, and Windows.

[return to main page]