Ubuntu Manpage: Spin − verification of multithreaded systems

NAME

        Spin − verification of multithreaded systems

SYNOPSIS

       spin -V
       spin [ options ] file

DESCRIPTION

SPIN is a tool for analyzing the logical consistency of asynchronous systems, specifically
distributed software, multi-threaded systems, and communication protocols. A model of the
system is specified in a guarded command language called Promela (process meta language).
This modeling language supports dynamic creation of processes, nondeterministic case
selection, loops, gotos, local 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 verification of the correctness requirements for the system. The main options
supported are as follows. (You can always get a full list of current options with the
command "spin --".

-a Generate a verifier (a model checker) for the specification. The output is written
into a set of C files named pan.[cbhmt], that can be compiled (cc -o pan pan.c) to
produce an executable verifier. The online SPIN manuals contain the details on
compilation and use of the verifiers.

-b Do not execute printf statements in a simulation run.

-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.

-Dxxx Pass -Dxxx to the preprocessor (see also -E and -I).

-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 variables, the 3rd field defines the name of the structure
declaration that contains the variable.

-Exxx Pass xxx to the preprocessor (see also -D and -I).

-e If the specification contains multiple never claims, or ltl properties, compute the
synchronous product of all claims and write the result to the standard output.

-f LTL Translate the LTL formula LTL into a never claim.
This option reads a formula in LTL syntax from the second argument and translates
it into Promela syntax (a never claim, qhich is Promela's equivalent of a Büchi
Automaton). The LTL operators 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.
This option has largely been replaced with the support for inline specification of
ltl formula, in Spin version 6.0.

-F file
Translate the LTL formula stored in file into a never claim.
This behaves identical 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 conventions of
the shell complicate the use of option -f . Option -F is meant to solve those
problems.)

-g In combination with option -p, print all global variable updates in a simulation
run.

-h At the end of a simulation run, print the value of the seed that was used for the
random number generator. By specifying the same seed with the -n option, the exact
run can be repeated later.

-I Show the result of inlining and preprocessing.

-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.

-jN Skip printing for the first N steps in a simulation run.

-J Reverse the evaluation order for nested unless statements, e.g., to match the way
in which Java handles exceptions.

-k file
Use the file name file as the trail-file, see also -t.

-l In combination with option -p, include all local variable updates in the output of
a simulation run.

-M Produce a message sequence chart in tcl/tk form for a random simulation or a guided
simulation (when combined with -t), for the model in file , and display the result
with wish. 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. ,TP -N file Use the never claim stored in file
to generate the verified (see -a).

-O Use the original scope rules from pre-Spin version 6.

-o[123]
Turn off data-flow optimization (-o1). Do not hide write-only variables (-o2)
during verification. Turn off statement merging (-o3) during verification. Turn
on rendezvous optimization (-o4) during verification. Turn on case caching (-o5)
to reduce the size of pan.m, but losing accuracy in reachability reports.

-O Use the scope rules pre-version 6.0. In this case there are only two possible
levels of scope for all data declarations: global, or proctype local. In version
6.0 and later there is a third level of scope: inlines or blocks.

-Pxxx Use the command xxx for preprocessing instead of the standard C preprocessor.

-p Include all statement executions in the output of simulation runs.

-qN Suppress the output generated for channel N during simulation runs.

-r Show all message-receive events, giving the name and number of the receiving
process and the corresponding the source line number. For each message parameter,
show the message type and the message channel number and name.

-replay
Replay an error trace found in an earlier verification (see -search). As with
-search, arguments meant for Spin itself (e.g., -p) can be given before the -replay
argument. If the replay can only be done with the ./pan executable, then arguments
for the replay with the ./pan executable can be given after the -replay argument.

-search
Compile and run directly. Verificaiton compile-time and runtime flags can be added
after this parameter. Any Spin parse-time parameters must come before the -search
parameter. The actual command line executed is printed if -v is specified (before
the -search argument).

-s Include all send operations in the output of simulation runs.

-T Do not automatically indent the printf output of process i with i tabs.

-t[N] Perform a guided simulation, following the [Nth] error trail that was produces by
an earlier verification run, see the online manuals for the details on
verification. By default the error trail is looked for in a file with the same
basename as the model, and with extension .trail. See also -k.

-v Verbose mode, add some more detail, and generate more hints and warnings about the
model.

-V Print the SPIN version number and exit.

-x Generate transition tables from model and exit (generates, compiles, and runs
pan.c).

With only a filename as an argument and no option flags, SPIN performs a random simulation
of the model specified in the file. This normally does not generate output, except what
is generated explicitly by the user within the model with printf statements, and some
details about the final state that is reached after the simulation completes. The group
of options -bgilmprstv is used to set the desired level of information that the user wants
about a random, guided, or interactive simulation run. Every line of output normally
contains a reference to the source line in the specification that generated it. If option
-i is included, the simulation is interactive, or if option -t or -k file is added, the
simulation is guided.

-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.

-s Show all message-send events.

-v Verbose mode, add some more detail, and generat more hints and warnings about the
model.

NAME

SYNOPSIS

DESCRIPTION

SEE ALSO