term% cat index.txt SPIN(1) General Commands Manual SPIN(1)
NAME
spin - verification tool for models of concurrent systems
SYNOPSIS
spin -a [ -m ] [ -Pcpp ] file
spin [ -bglmprsv ] [ -nN ] [ -Pcpp ] file
spin -c [ -t ] [ -Pcpp ] file
spin -d [ -Pcpp ] file
spin -f ltl
spin -F file
spin -i [ -bglmprsv ] [ -nN ] [ -Pcpp ] file
spin -M [ -t ] [ -Pcpp ] file
spin -t[N] [ -bglmprsv ] [ -jN ] [ -Pcpp ] file
spin -V
DESCRIPTION
Spin is a tool for analyzing the logical consistency of asynchronous
systems, specifically distributed software and communication protocols.
A verification model of the system is first specified in a guarded com‐
mand language called Promela. This specification language, described
in the reference, allows for the modeling of dynamic creation of asyn‐
chronous processes, nondeterministic case selection, loops, gotos, lo‐
cal and global variables. It also allows for a concise specification
of logical correctness requirements, including, but not restricted to,
requirements expressed in linear temporal logic.
Given a Promela model stored in file, spin can perform interactive,
guided, or random simulations of the system's execution. It can also
generate a C program that performs an exhaustive or approximate verifi‐
cation of the correctness requirements for the system.
-a Generate a verifier (model checker) for the specification. The
output is written into a set of C files, named pan.[cbhmt], that
can be compiled (pcc pan.c) to produce an executable verifier.
The online spin manuals (see below) contain the details on com‐
pilation and use of the verifiers.
-c Produce an ASCII approximation of a message sequence chart for a
random or guided (when combined with -t) simulation run. See
also option -M.
-d Produce symbol table information for the model specified in
file. For each Promela object this information includes the
type, name and number of elements (if declared as an array), the
initial value (if a data object) or size (if a message channel),
the scope (global or local), and whether the object is declared
as a variable or as a parameter. For message channels, the data
types of the message fields are listed. For structure vari‐
ables, the third field defines the name of the structure decla‐
ration that contains the variable.
-f ltl Translate the LTL formula ltl into a never claim.
This option reads a formula in LTL syntax from the second argu‐
ment and translates it into Promela syntax (a never claim, which
is Promela's equivalent of a Büchi Automaton). The LTL opera‐
tors are written: [] (always), <> (eventually), and U (strong
until). There is no X (next) operator, to secure compatibility
with the partial order reduction rules that are applied during
the verification process. If the formula contains spaces, it
should be quoted to form a single argument to the spin command.
-F file
Translate the LTL formula stored in file into a never claim.
This behaves identically to option -f but will read the formula
from the file instead of from the command line. The file should
contain the formula as the first line. Any text that follows
this first line is ignored, so it can be used to store comments
or annotation on the formula. (On some systems the quoting con‐
ventions of the shell complicate the use of option -f. Option
-F is meant to solve those problems.)
-i Perform an interactive simulation, prompting the user at every
execution step that requires a nondeterministic choice to be
made. The simulation proceeds without user intervention when
execution is deterministic.
-M Produce a message sequence chart in Postscript form for a random
simulation or a guided simulation (when combined with -t), for
the model in file, and write the result into file.ps. See also
option -c.
-m Changes the semantics of send events. Ordinarily, a send action
will be (blocked) if the target message buffer is full. With
this option a message sent to a full buffer is lost.
-nN Set the seed for a random simulation to the integer value N.
There is no space between the -n and the integer N.
-t Perform a guided simulation, following the error trail that was
produces by an earlier verification run, see the online manuals
for the details on verification.
-V Prints the spin version number and exits.
With only a filename as an argument and no options, spin performs a
random simulation of the model specified in the file (standard input is
the default if the filename is omitted). If option -i is added, the
simulation is interactive, or if option -t is added, the simulation is
guided.
The simulation normally does not generate output, except what is gener‐
ated explicitly by the user within the model with printf statements,
and some details about the final state that is reached after the simu‐
lation completes. The group of options -bglmprsv sets the desired
level of information that the user wants about a random, guided, or in‐
teractive simulation run. Every line of output normally contains a
reference to the source line in the specification that generated it.
-b Suppress the execution of printf statements within the model.
-g Show at each time step the current value of global variables.
-l In combination with option -p, show the current value of local
variables of the process.
-p Show at each simulation step which process changed state, and
what source statement was executed.
-r Show all message-receive events, giving the name and number of
the receiving process and the corresponding the source line num‐
ber. For each message parameter, show the message type and the
message channel number and name.
-s Show all message-send events.
-v Verbose mode, add some more detail, and generate more hints and
warnings about the model.
SOURCE
/sys/src/cmd/spin
SEE ALSO
http://spinroot.com: GettingStarted.pdf, Roadmap.pdf, Manual.pdf, What‐
sNew.pdf, Exercises.pdf
G.J. Holzmann, Design and Validation of Computer Protocols, Prentice
Hall, 1991.
â, `Design and validation of protocols: a tutorial,' Computer Networks
and ISDN Systems, Vol. 25, No. 9, 1993, pp. 981-1017.
â, `The model checker Spin,' IEEE Trans. on SE, Vol, 23, No. 5, May
1997.
SPIN(1)