+++ /dev/null
-.ds Z S\s-2PIN\s0
-.ds P P\s-2ROMELA\s0
-.\"
-.\" On CYGWIN move this page to c:/cygwin/usr/man/man1/spin.1
-.\"
-.TH SPIN 1
-.CT 1 comm_mach protocol
-.SH NAME
-spin \(mi verification tool for models of concurrent systems
-.SH SYNOPSIS
-.B spin
-.BI "-a [-m]"
-[
-.BI -P cpp
-]
-.I file
-.br
-.B spin
-.BI "[-bglmprsv] [-n\f2N\f(BI]"
-[
-.BI -P cpp
-]
-.I file
-.br
-.B spin
-.BI "-c [-t]"
-[
-.BI -P cpp
-]
-.I file
-.br
-.B spin
-.BI -d
-[
-.BI -P cpp
-]
-.I file
-.br
-.B spin
-.BI -f
-.I LTL
-.br
-.B spin
-.BI -F
-.I file
-.br
-.B spin
-.BI "-i [-bglmprsv] [-n\f2N\f(BI]"
-[
-.BI -P cpp
-]
-.I file
-.br
-.B spin
-.BI "-M [-t]"
-[
-.BI -P cpp
-]
-.I file
-.br
-.B spin
-.BI "-t[N] [-bglmprsv] [-j\f2N\f(BI]"
-[
-.BI -P cpp
-]
-.I file
-.br
-.B spin
-.BI -V
-.I file
-.SH DESCRIPTION
-\*Z
-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 ,
-\*Z 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.
-.\"----------------------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 ( "cc pan.c" )
-to produce an executable verifier.
-The online \*Z 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 \19(when combined with \f3-t\f1)
-simulation run. See also option \f3-M\f1.
-.\"--------------------------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 3rd field defines the
-name of the structure declaration that contains the variable.
-.\"--------------------------f------------
-.TP
-.BI "-f \f2LTL\f1"
-Translate the LTL formula \f2LTL\f1 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, qhich is Promela's
-equivalent of a B\(u"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 \*Z command.
-.\"--------------------------F------------
-.TP
-.BI "-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
-.B -f .
-Option
-.B -F
-is meant to solve those problems.)
-.\"--------------------------i------------
-.TP
-.BI -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
-.BI -M
-Produce a message sequence chart in Postscript form for a
-random simulation or a guided simulation
-(when combined with \f(BI-t\f1), for the model in
-.I file ,
-and write the result into
-.I file.ps .
-See also option \f3-c\f1.
-.\"--------------------------m------------
-.TP
-.BI -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
-.BI "-n\f2N"
-Set the seed for a random simulation to the integer value
-.I N .
-There is no space between the \f(BI-n\f1 and the integer \f2N\f1.
-.\"--------------------------t------------
-.TP
-.BI -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
-.BI -V
-Prints the \*Z version number and exits.
-.\"--------------------------.------------
-.PP
-With only a filename as an argument and no option flags,
-\*Z 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 \f(CWprintf\f1
-statements, and some details about the final state that is
-reached after the simulation completes.
-The group of options
-.B -bglmprsv
-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
-.B -i
-is added, the simulation is \f2interactive\f1, or if option
-.B -t
-is added, the simulation is \f2guided\f1.
-.\"--------------------------bglprsv------------
-.TP
-.BI -b
-Suppress the execution of \f(CWprintf\f1 statements within the model.
-.TP
-.BI -g
-Show at each time step the current value of global variables.
-.TP
-.BI -l
-In combination with option
-.BR -p ,
-show the current value of local variables of the process.
-.TP
-.BI -p
-Show at each simulation step which process changed state,
-and what source statement was executed.
-.TP
-.BI -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
-.BI -s
-Show all message-send events.
-.TP
-.BI -v
-Verbose mode, add some more detail, and generat more
-hints and warnings about the model.
-.SH SEE ALSO
-Online manuals at spinroot.com:
-.br
-.in +4
-GettingStarted.pdf,
-Roadmap.pdf,
-Manual.pdf,
-WhatsNew.pdf,
-Exercises.pdf
-.in -4
-More background information on the system and the verification process,
-can be found in, for instance:
-.br
-.in +4
-G.J. Holzmann, \f2Design and Validation of Computer Protocols\f1,
-Prentice Hall, 1991.
-.br
---, `Design and validation of protocols: a tutorial,'
-\f2Computer Networks and ISDN Systems\f1,
-Vol. 25, No. 9, 1993, pp. 981-1017.
-.br
---, `The model checker \*Z,'
-\f2IEEE Trans. on SE\f1, Vol, 23, No. 5, May 1997.
-.in -4
-.br
\ No newline at end of file
projects / lttv.git / blobdiff