spin – verification tool for models of concurrent systems|
spin [ options ] file|
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
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 ––").
–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.
–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 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.
–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.
–oTurn 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
–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.
–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 Prints the spin version number and exit.
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 i interactive, or if option –t or –kfile is added, the
simulation is guided.
G.J. Holzmann, The Spin Model Checker (Primer and Reference Manual), .}f Addison–Wesley, Reading, Mass., 2004.
—, `The model checker Spin,' IEEE Trans. on SE, Vol, 23, No. 5, May 1997.
—, `Design and validation of protocols: a tutorial,' Computer Networks and ISDN Systems, Vol. 25, No. 9, 1993, pp. 981–1017.
—, Design and Validation of Computer Protocols, Prentice Hall, Englewood Cliffs, NJ, 1991.