Spin is an open-source model-checker that can be used for the formal verification of distributed software systems. Spin has been developed at Bell Labs, in the Computing Sciences Research Center, starting in 1980. It has been available freely since 1991, and was awarded the prestigious System Software Award for 2001 by the ACM in April 2002.
Spin is used to trace logical design errors in distributed systems design (such as operating systems, data communications protocols, etc.) and checks the logical consistency of a given specification. This specification is described in a high level language called Promela (PROcess or PROtocol MEta LAnguage). The language allows for the dynamic creation of concurrent processes, which communicate through synchronous or asynchronous message channels, or via shared memory.
The tool is used to verify correctness properties. Those properties can be specified in different ways: 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. Spin can also automatically report on deadlocks, unspecified receptions, race conditions, or unexecutable code.
The simulation of the specification in Promela can be interactive or random. Spin can also produce a C program that will perform a fast exhaustive verification of the system state space. Proof techniques are both exhaustive and partial, and based on either depth-first or breadth-first search. Spin is specifically designed to scale well, and to handle even very large problem sizes efficiently.
Spin can also be used as an exhaustive verifier, capable of rigorously proving the validity of user specified correctness requirements (using partial order reduction theory to optimise the search) or as a proof approximation system that can validate even very large system models with maximal coverage of the state space.
Promela (PROcess or PROtocol MEta LAnguage) is the input language of Spin. 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.
A specification in Promela consists of three types of objects:
It is standard to divide correctness properties in two kinds: safety properties (the bad things that should be avoided) and liveness properties (the good things that should happen). As it is difficult to define what is good or bad, correctness properties with Promela are defined with two types of correctness claims: state properties (ie claims about (un)reachable states) and path properties (ie claims about (in)feasible executions). They use the following constructs:
For example, the following code, from the book The Spin Model Checker, specifies two processes using a rendez-vous mechanism to synchronise:
/* mychannel is a channel of capacity 0:
* it defines a rendez-vous mechanism between the processes A and B
* (the sender, A, is blocked until the receiver, B, is performing the reception)
*/
mtype = { msgname };
chan mychannel [0] of {mtype, byte};
active proctype A()
{
mychannel!msgname(124);
/* The following is unexecutable:
no matching receive at B, and capacity of channel = 0 */
mychannel!msgname(125);
}
active proctype B()
{
byte state;
mychannel?msgname(state);
/* correctness property using an assertion */
assert (state == 124);
}
Spin runs on Unix systems, Mac (MacOSX) and Windows PCs (Windows 95 or later). See the installation instructions at: http://spinroot.com/spin/Man/README.html.
XSpin is a optional graphical front-end for Spin, written in Tcl/Tk. Its use is highly recommended. It should be available with the Spin distribution.
Some reading material include:
