3 spin - verification tool for models of concurrent systems
92 is a tool for analyzing the logical consistency of
93 asynchronous systems, specifically distributed software
94 amd communication protocols.
95 A verification model of the system is first specified
96 in a guarded command language called
98 This specification language, described in the reference,
99 allows for the modeling of dynamic creation of
100 asynchronous processes,
101 nondeterministic case selection, loops, gotos, local and
103 It also allows for a concise specification of logical
104 correctness requirements, including, but not restricted
105 to requirements expressed in linear temporal logic.
107 Given a Promela model stored in
110 can perform interactive, guided, or random simulations
111 of the system's execution.
112 It can also generate a C program that performs an exhaustive
113 or approximate verification of the correctness requirements
118 Generate a verifier (model checker) for the specification.
119 The output is written into a set of C files, named
123 to produce an executable verifier.
126 manuals (see below) contain
127 the details on compilation and use of the verifiers.
131 Produce an ASCII approximation of a message sequence
132 chart for a random or guided (when combined with
134 simulation run. See also option
139 Produce symbol table information for the model specified in
141 For each Promela object this information includes the type, name and
142 number of elements (if declared as an array), the initial
143 value (if a data object) or size (if a message channel), the
144 scope (global or local), and whether the object is declared as
145 a variable or as a parameter. For message channels, the data types
146 of the message fields are listed.
147 For structure variables, the third field defines the
148 name of the structure declaration that contains the variable.
152 Translate the LTL formula
158 This option reads a formula in LTL syntax from the second argument
159 and translates it into Promela syntax (a
161 claim, which is Promela's
162 equivalent of a Büchi Automaton).
163 The LTL operators are written:
170 (strong until). There is no
172 (next) operator, to secure
173 compatibility with the partial order reduction rules that are
174 applied during the verification process.
175 If the formula contains spaces, it should be quoted to form a
176 single argument to the
182 Translate the LTL formula stored in
188 This behaves identically to option
190 but will read the formula from the
192 instead of from the command line.
193 The file should contain the formula as the first line. Any text
194 that follows this first line is ignored, so it can be used to
195 store comments or annotation on the formula.
196 (On some systems the quoting conventions of the shell complicate
201 is meant to solve those problems.)
205 Perform an interactive simulation, prompting the user at
206 every execution step that requires a nondeterministic choice
207 to be made. The simulation proceeds without user intervention
208 when execution is deterministic.
212 Produce a message sequence chart in Postscript form for a
213 random simulation or a guided simulation
218 and write the result into
225 Changes the semantics of send events.
226 Ordinarily, a send action will be (blocked) if the
227 target message buffer is full.
228 With this option a message sent to a full buffer is lost.
232 Set the seed for a random simulation to the integer value
234 There is no space between the
241 Perform a guided simulation, following the error trail that
242 was produces by an earlier verification run, see the online manuals
243 for the details on verification.
249 version number and exits.
252 With only a filename as an argument and no options,
254 performs a random simulation of the model specified in
255 the file (standard input is the default if the filename is omitted).
258 is added, the simulation is
262 is added, the simulation is
265 The simulation normally does not generate output, except what is generated
266 explicitly by the user within the model with
268 statements, and some details about the final state that is
269 reached after the simulation completes.
272 sets the desired level of information that the user wants
273 about a random, guided, or interactive simulation run.
274 Every line of output normally contains a reference to the source
275 line in the specification that generated it.
279 Suppress the execution of
281 statements within the model.
284 Show at each time step the current value of global variables.
287 In combination with option
289 show the current value of local variables of the process.
292 Show at each simulation step which process changed state,
293 and what source statement was executed.
296 Show all message-receive events, giving
297 the name and number of the receiving process
298 and the corresponding the source line number.
299 For each message parameter, show
300 the message type and the message channel number and name.
303 Show all message-send events.
306 Verbose mode, add some more detail, and generate more
307 hints and warnings about the model.
313 .BR http://spinroot.com :
314 .BR GettingStarted.pdf ,
322 .IR "Design and Validation of Computer Protocols" ,
325 —, `Design and validation of protocols: a tutorial,'
326 .IR "Computer Networks and ISDN Systems" ,
327 Vol. 25, No. 9, 1993, pp. 981-1017.
329 —, `The model checker Spin,'
330 .IR "IEEE Trans. on SE" ,
331 Vol, 23, No. 5, May 1997.