123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331 |
- .TH SPIN 1
- .SH NAME
- spin \- verification tool for models of concurrent systems
- .SH SYNOPSIS
- .B spin
- .B -a
- [
- .B -m
- ]
- [
- .BI -P cpp
- ]
- .I file
- .PP
- .B spin
- [
- .B -bglmprsv
- ]
- [
- .BI -n N
- ]
- [
- .BI -P cpp
- ]
- .I file
- .PP
- .B spin
- .B -c
- [
- .B -t
- ]
- [
- .BI -P cpp
- ]
- .I file
- .PP
- .B spin
- .B -d
- [
- .BI -P cpp
- ]
- .I file
- .PP
- .B spin
- .B -f
- .I ltl
- .PP
- .B spin
- .B -F
- .I file
- .PP
- .B spin
- .B -i
- [
- .B -bglmprsv
- ]
- [
- .BI -n N
- ]
- [
- .BI -P cpp
- ]
- .I file
- .PP
- .B spin
- .B -M
- [
- .B -t
- ]
- [
- .BI -P cpp
- ]
- .I file
- .PP
- .B spin
- .BR -t [ \fIN ]
- [
- .B -bglmprsv
- ]
- [
- .BI -j N
- ]
- [
- .BI -P cpp
- ]
- .I file
- .PP
- .B spin
- .B -V
- .SH DESCRIPTION
- .I Spin
- is a tool for analyzing the logical consistency of
- asynchronous systems, specifically distributed software
- amd 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.
- .PP
- Given a Promela model
- stored in
- .I file ,
- .I 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.
- .PP
- The basic command options are:
- .\"----------------------a----------------
- .TP
- .B -a
- Generate a verifier (model checker) for the specification.
- The output is written into a set of C files, named
- .BR pan.[cbhmt] ,
- that can be compiled
- .RB ( "pcc pan.c" )
- to produce an executable verifier.
- The online
- .I spin
- manuals (see below) contain
- the details on compilation and use of the verifiers.
- .\"--------------------------c------------
- .TP
- .B -c
- Produce an ASCII approximation of a message sequence
- chart for a random or guided (when combined with
- .BR -t )
- simulation run.
- See also option
- .BR -M .
- .\"--------------------------d------------
- .TP
- .BI -d
- Produce symbol table information for the model specified in
- .I 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 third field defines the
- name of the structure declaration that contains the variable.
- .\"--------------------------f------------
- .TP
- .B "-f \f2ltl\f1"
- Translate the LTL formula
- .I ltl
- into a never claim.
- .br
- This option reads a formula in LTL syntax from the second argument
- and translates it into Promela syntax (a never claim, which is Promela's
- equivalent of a Büchi Automaton).
- The LTL operators are written:
- .B []
- (always),
- .B <>
- (eventually),
- and
- .B U
- (strong until). There is no
- .B 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
- .I spin
- command.
- .\"--------------------------F------------
- .TP
- .B "-F \f2file\f1"
- Translate the LTL formula stored in
- .I file
- into a never claim.
- .br
- This behaves identical to option
- .B -f
- but will read the formula from the
- .I 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
- .BR -f .
- Option
- .B -F
- is meant to solve those problems.)
- .\"--------------------------i------------
- .TP
- .B -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------------
- .TP
- .B -M
- Produce a message sequence chart in Postscript form for a
- random simulation or a guided simulation
- (when combined with
- .BR -t ),
- for the model in
- .I file ,
- and write the result into
- .I file.ps .
- See also option
- .BR -c .
- .\"--------------------------m------------
- .TP
- .B -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.
- .\"--------------------------n------------
- .TP
- .B "-n\f2N"
- Set the seed for a random simulation to the integer value
- .I N .
- There is no space between the
- .B -n
- and the integer
- .IR N .
- .\"--------------------------t------------
- .TP
- .B -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------------
- .TP
- .B -V
- Prints the
- .I spin
- version number and exits.
- .\"--------------------------.------------
- .PD
- .PP
- With only a filename as an argument and no option flags,
- .I spin
- performs a random simulation of the model specified in
- the file (standard input is the default if the filename is omitted).
- If option
- .B -i
- is added, the simulation is
- .IR interactive ,
- or if option
- .B -t
- is added, the simulation is
- .IR guided .
- .PP
- The simulation normally does not generate output, except what is generated
- explicitly by the user within the model with
- .B printf
- statements, and some details about the final state that is
- reached after the simulation completes.
- The group of options
- .B -bglprsv
- 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.
- The options are:
- .\"--------------------------bglprsv------------
- .TP
- .B -b
- Suppress the execution of
- .B printf
- statements within the model.
- .TP
- .B -g
- Show at each time step the current value of global variables.
- .TP
- .B -l
- In combination with option
- .BR -p ,
- show the current value of local variables of the process.
- .TP
- .B -p
- Show at each simulation step which process changed state,
- and what source statement was executed.
- .TP
- .B -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.
- .TP
- .B -s
- Show all message-send events.
- .TP
- .B -v
- Verbose mode, add some more detail, and generat more
- hints and warnings about the model.
- .PD
- .SH SOURCE
- .B /sys/src/cmd/spin
- .SH SEE ALSO
- G.J. Holzmann,
- .IR "Design and Validation of Computer Protocols" ,
- Prentice Hall, 1991.
- .br
- \(em, ``Design and validation of protocols: a tutorial,''
- .I "Computer Networks and ISDN Systems" ,
- Vol. 25, No. 9, 1993, pp. 981-1017.
- .br
- \(em, ``The model checker
- .SM SPIN\c
- \&,''
- .I "IEEE Trans. on Software Engineering" ,
- Vol, 23, No. 5, May 1997.
- .br
- \(em, ``Using
- .SM SPIN\c
- \&,''
- this manual.
- .PP
- .B http://spinroot.com/
|