Spin and Promela

Model checking with Spin

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

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:

  • processes. They consist of data and channel declarations and statements that specify a behaviour. They are declared with proctype.
  • data objects are declared global or local to processes, using a C-like syntax. Basic data types are supported (such as integers, booleans, …) as well as structured data types.
  • message channels are also declared globally or locally within a process. They are used to model the exchange of data between processes. Sending and receiving on a channel are respectively specified using the ! and ? syntax from CSP. my_channel!msg_name(expr1, expr2) sends a message msg_name with two arguments. Reception of such a message would be: my_channel?msg_name(var1, var2).

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:

  • basic assertions (boolean expressions that must evaluate to TRUE)
  • end-state labels (to distinguish valid end states from invalid ones like deadlocks)
  • progress-state labels (to mark statements that accomplish something desirable, or good)
  • accept-state labels (used to formalise Büchi acceptance conditions. They are used to specify fairness conditions: an accept state cannot be visited infinitely often)
  • never claims (behaviour that should never occur)
  • trace assertions (specifies valid or invalid sequences of operations that processes can perform on message channels)

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 tool support and resources

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: