verif/Spin/Man/spin.1

   1 .ds Z S\s-2PIN\s0
   2 .ds P P\s-2ROMELA\s0
   3 .\"
   4 .\" On CYGWIN move this page to c:/cygwin/usr/man/man1/spin.1
   5 .\"
   6 .TH SPIN 1
   7 .CT 1 comm_mach protocol
   8 .SH NAME
   9 spin \(mi verification tool for models of concurrent systems
  10 .SH SYNOPSIS
  11 .B spin
  12 .BI "-a [-m]"
  13 [
  14 .BI -P cpp
  15 ]
  16 .I file
  17 .br
  18 .B spin
  19 .BI "[-bglmprsv] [-n\f2N\f(BI]"
  20 [
  21 .BI -P cpp
  22 ]
  23 .I file
  24 .br
  25 .B spin
  26 .BI "-c [-t]"
  27 [
  28 .BI -P cpp
  29 ]
  30 .I file
  31 .br
  32 .B spin
  33 .BI -d
  34 [
  35 .BI -P cpp
  36 ]
  37 .I file
  38 .br
  39 .B spin
  40 .BI -f
  41 .I LTL
  42 .br
  43 .B spin
  44 .BI -F
  45 .I file
  46 .br
  47 .B spin
  48 .BI "-i [-bglmprsv] [-n\f2N\f(BI]"
  49 [
  50 .BI -P cpp
  51 ]
  52 .I file
  53 .br
  54 .B spin
  55 .BI "-M [-t]"
  56 [
  57 .BI -P cpp
  58 ]
  59 .I file
  60 .br
  61 .B spin
  62 .BI "-t[N] [-bglmprsv] [-j\f2N\f(BI]"
  63 [
  64 .BI -P cpp
  65 ]
  66 .I file
  67 .br
  68 .B spin
  69 .BI -V
  70 .I file
  71 .SH DESCRIPTION
  72 \*Z
  73 is a tool for analyzing the logical consistency of
  74 asynchronous systems, specifically distributed software
  75 amd communication protocols.
  76 A verification model of the system is first specified
  77 in a guarded command language called Promela.
  78 This specification language, described in the reference,
  79 allows for the modeling of dynamic creation of
  80 asynchronous processes,
  81 nondeterministic case selection, loops, gotos, local and
  82 global variables.
  83 It also allows for a concise specification of logical
  84 correctness requirements, including, but not restricted
  85 to requirements expressed in linear temporal logic.
  86 .PP
  87 Given a Promela model
  88 stored in
  89 .I file ,
  90 \*Z can perform interactive, guided, or random simulations
  91 of the system's execution.
  92 It can also generate a C program that performs an exhaustive
  93 or approximate verification of the correctness requirements
  94 for the system.
  95 .\"----------------------a----------------
  96 .TP
  97 .B -a
  98 Generate a verifier (model checker) for the specification.
  99 The output is written into a set of C files, named
 100 .BR pan. [ cbhmt ],
 101 that can be compiled
 102 .RB ( "cc pan.c" )
 103 to produce an executable verifier.
 104 The online \*Z manuals (see below) contain
 105 the details on compilation and use of the verifiers.
 106 .\"--------------------------c------------
 107 .TP
 108 .B -c
 109 Produce an ASCII approximation of a message sequence
 110 chart for a random or guided \19(when combined with \f3-t\f1)
 111 simulation run. See also option \f3-M\f1.
 112 .\"--------------------------d------------
 113 .TP
 114 .BI -d
 115 Produce symbol table information for the model specified in
 116 .I file .
 117 For each Promela object this information includes the type, name and
 118 number of elements (if declared as an array), the initial
 119 value (if a data object) or size (if a message channel), the
 120 scope (global or local), and whether the object is declared as
 121 a variable or as a parameter.  For message channels, the data types
 122 of the message fields are listed.
 123 For structure variables, the 3rd field defines the
 124 name of the structure declaration that contains the variable.
 125 .\"--------------------------f------------
 126 .TP
 127 .BI "-f \f2LTL\f1"
 128 Translate the LTL formula \f2LTL\f1 into a never claim.
 129 .br
 130 This option reads a formula in LTL syntax from the second argument
 131 and translates it into Promela syntax (a never claim, qhich is Promela's
 132 equivalent of a B\(u"chi Automaton).
 133 The LTL operators are written: [] (always), <> (eventually),
 134 and U (strong until).  There is no X (next) operator, to secure
 135 compatibility with the partial order reduction rules that are
 136 applied during the verification process.
 137 If the formula contains spaces, it should be quoted to form a
 138 single argument to the \*Z command.
 139 .\"--------------------------F------------
 140 .TP
 141 .BI "-F \f2file\f1"
 142 Translate the LTL formula stored in
 143 .I file
 144 into a never claim.
 145 .br
 146 This behaves identical to option
 147 .B -f
 148 but will read the formula from the
 149 .I file
 150 instead of from the command line.
 151 The file should contain the formula as the first line.  Any text
 152 that follows this first line is ignored, so it can be used to
 153 store comments or annotation on the formula.
 154 (On some systems the quoting conventions of the shell complicate
 155 the use of option
 156 .B -f .
 157 Option
 158 .B -F
 159 is meant to solve those problems.)
 160 .\"--------------------------i------------
 161 .TP
 162 .BI -i
 163 Perform an interactive simulation, prompting the user at
 164 every execution step that requires a nondeterministic choice
 165 to be made.  The simulation proceeds without user intervention
 166 when execution is deterministic.
 167 .\"--------------------------M------------
 168 .TP
 169 .BI -M
 170 Produce a message sequence chart in Postscript form for a
 171 random simulation or a guided simulation
 172 (when combined with \f(BI-t\f1), for the model in
 173 .I file ,
 174 and write the result into
 175 .I file.ps .
 176 See also option \f3-c\f1.
 177 .\"--------------------------m------------
 178 .TP
 179 .BI -m
 180 Changes the semantics of send events.
 181 Ordinarily, a send action will be (blocked) if the
 182 target message buffer is full.
 183 With this option a message sent to a full buffer is lost.
 184 .\"--------------------------n------------
 185 .TP
 186 .BI "-n\f2N"
 187 Set the seed for a random simulation to the integer value
 188 .I N .
 189 There is no space between the \f(BI-n\f1 and the integer \f2N\f1.
 190 .\"--------------------------t------------
 191 .TP
 192 .BI -t
 193 Perform a guided simulation, following the error trail that
 194 was produces by an earlier verification run, see the online manuals
 195 for the details on verification.
 196 .\"--------------------------V------------
 197 .TP
 198 .BI -V
 199 Prints the \*Z version number and exits.
 200 .\"--------------------------.------------
 201 .PP
 202 With only a filename as an argument and no option flags,
 203 \*Z performs a random simulation of the model specified in
 204 the file (standard input is the default if the filename is omitted).
 205 This normally does not generate output, except what is generated
 206 explicitly by the user within the model with \f(CWprintf\f1
 207 statements, and some details about the final state that is
 208 reached after the simulation completes.
 209 The group of options
 210 .B -bglmprsv
 211 is used to set the desired level of information that the user wants
 212 about a random, guided, or interactive simulation run.
 213 Every line of output normally contains a reference to the source
 214 line in the specification that generated it.
 215 If option
 216 .B -i
 217 is added, the simulation is \f2interactive\f1, or if option
 218 .B -t
 219 is added, the simulation is \f2guided\f1.
 220 .\"--------------------------bglprsv------------
 221 .TP
 222 .BI -b
 223 Suppress the execution of \f(CWprintf\f1 statements within the model.
 224 .TP
 225 .BI -g
 226 Show at each time step the current value of global variables.
 227 .TP
 228 .BI -l
 229 In combination with option
 230 .BR -p ,
 231 show the current value of local variables of the process.
 232 .TP
 233 .BI -p
 234 Show at each simulation step which process changed state,
 235 and what source statement was executed.
 236 .TP
 237 .BI -r
 238 Show all message-receive events, giving
 239 the name and number of the receiving process
 240 and the corresponding the source line number.
 241 For each message parameter, show
 242 the message type and the message channel number and name.
 243 .TP
 244 .BI -s
 245 Show all message-send events.
 246 .TP
 247 .BI -v
 248 Verbose mode, add some more detail, and generat more
 249 hints and warnings about the model.
 250 .SH SEE ALSO
 251 Online manuals at spinroot.com:
 252 .br
 253 .in +4
 254 GettingStarted.pdf,
 255 Roadmap.pdf,
 256 Manual.pdf,
 257 WhatsNew.pdf,
 258 Exercises.pdf
 259 .in -4
 260 More background information on the system and the verification process,
 261 can be found in, for instance:
 262 .br
 263 .in +4
 264 G.J. Holzmann, \f2Design and Validation of Computer Protocols\f1,
 265 Prentice Hall, 1991.
 266 .br
 267 --, `Design and validation of protocols: a tutorial,'
 268 \f2Computer Networks and ISDN Systems\f1,
 269 Vol. 25, No. 9, 1993, pp. 981-1017.
 270 .br
 271 --, `The model checker \*Z,'
 272 \f2IEEE Trans. on SE\f1, Vol, 23, No. 5, May 1997.
 273 .in -4
 274 .br