term% cat index.txt SPIN(1) General Commands Manual SPIN(1)
NAME
spin - verification tool for concurrent systems
SYNOPSIS
spin [ -nN ] [ -plgrsmv ] [ -iat ] [ -DV ] [ file ]
DESCRIPTION
Spin is a tool for analyzing the logical consistency of concurrent sys‐
tems, 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, nondeter‐
ministic case selection, loops, gotos, variables, and the specification
of correctness requirements. The tool has fast algorithms for analyz‐
ing arbitrary liveness and safety conditions.
Given a model system specified in PROMELA2, spin can perform interac‐
tive, guided, or random simulations of the system's execution or it can
generate a C program that performs an exhaustive or approximate verifi‐
cation 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 value N.
The group of options -pglmrsv is used to set the level of information
reported about the simulation run. Every line of output normally con‐
tains 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 executed.
l In combination with option p, show the current value of local
variables of the process.
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 mes‐
sage 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 buf‐
fer is lost. The option can be combined 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 re‐
quire 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 op‐
tions pglrsv, different views of the error sequence are then be
obtained.
D Perform a static dataflow analysis.
V Print the version number and exit.
SEE ALSO
G.J. Holzmann, Design and Validation of Computer Protocols, Prentice
Hall, 1991.
—, ``Using SPIN''.
SPIN(1)