Spin Run-Time Options

Spin

Run-Time Options

Overview

NAME
spin - verification tool for models of distributed systems

SYNTAX
spin [options] 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 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.

Simulation Options

With only a filename as an argument and no option flags, Spin performs a random simulation of the model specified in the file (standard input is the default if the filename is omitted). 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. A first group of option flags can be used to set the desired level of information that the user wants to see in 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 added, the simulation is interactive, or if option -t is added, the simulation is guided.

Verifier Generation Related

Optimization

The following group of options controls which optimizations are enabled or disabled for verifier generation. By default most of the important optimizations are enabled.

SEE ALSO

More background information on the system and the verification process, can be found in:


Spin Online References
Promela Manual Index
Spin HomePage
(Page Updated: 28 November 2004)