spin - verification tool for concurrent systems
spin [ -nN ] [ -plgrsmv ] [ -iat ] [ -DV ] [ file ]
Spin is a tool for analyzing the logical consistency of concurrent systems, specifically
communication protocols. The system is specified in a guarded command language called
PROMELA2. The language, described in the references, allows for the dynamic creation of
processes, nondeterministic case selection, loops, gotos, variables, and the specification
of correctness requirements. The tool has fast algorithms for analyzing arbitrary live-
ness and safety conditions.
Given a model system specified in PROMELA2, spin can perform interactive, guided, or ran-
dom simulations of the system's execution or it can generate a C program that performs an
exhaustive or approximate verification of the system. The verifier can check, for
instance, if user specified system invariants are violated during a protocol's execution,
or if non-progress execution cycles exist.
Without any options the program performs a random simulation of the system defined in the
input file, default standard input. The option -nN sets the random seed to the integer
The group of options -pglmrsv is used to set the level of information reported about the
simulation run. Every line of output normally contains a reference to the source line in
the specification that caused it.
p Show at each time step which process changed state and what source statement was
l In combination with option p, show the current value of local variables of the
g Show the value of global variables at each time step.
r Show all message-receive events, giving the name and number of the receiving
process and the corresponding source line number. For each message parameter, show
the message type and the message channel number and name.
s Show all message-send events.
m Ordinarily, a send action will be delayed if the target message buffer if full.
With this option a message sent to a full buffer is lost. The option can be com-
bined with -a (see below).
v Verbose mode: add extra detail and include more warnings.
i Perform an interactive simulation.
a Generate a protocol-specific verifier. The output is written into a set of C
files, named pan.[cbhmt], that can be compiled (cc pan.c) to produce an executable
verifier. Systems that require more memory than available on the target machine
can still be analyzed by compiling the verifier with a bit state space:
cc -DBITSTATE pan.c
This collapses the state space to 1 bit per system state, with minimal side-
effects. Partial order reduction rules take effect during the verification if the
compiler directive -DREDUCE is used.
The compiled verifiers have their own sets of options, which can be seen by running
them with option -?.
t If the verifier finds a violation of a correctness property, it writes an error
trail. The trail can be inspected in detail by invoking spin with the -t option.
In combination with the options pglrsv, different views of the error sequence are
then be obtained.
D Perform a static dataflow analysis.
V Print the version number and exit.
G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
--, ``Using SPIN''.