spin – verification tool for models of concurrent systems|
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 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
command language called Promela. This specification language,
described in the reference, allows for the
modeling of dynamic creation of asynchronous 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 or approximate
verification of the correctness requirements for the system.
–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 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 –bglmprsv
sets 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.
http://spinroot.com: GettingStarted.pdf, Roadmap.pdf, Manual.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.