![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to spin CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Plan 9 NeXT] / lucent / sys / man / 1|
Return to spin CVS log | Up to [Plan 9 NeXT] / lucent / sys / man / 1 |
1.1 root 1: .TH SPIN 1
2: .SH NAME
3: spin \- verification tool for concurrent systems
4: .SH SYNOPSIS
5: .B spin
6: [
7: .BI -n N
8: ]
9: [
10: .B -plgrsmv
11: ]
12: [
13: .B -iat
14: ]
15: [
16: .B -DV
17: ]
18: [
19: .I file
20: ]
21: .SH DESCRIPTION
22: .I Spin
23: is a tool for analyzing the logical consistency of
24: concurrent systems, specifically communication protocols.
25: The system is specified in a guarded command language called
26: .SM PROMELA2\c
27: \&.
28: The language, described in the references,
29: allows for the dynamic creation of processes,
30: nondeterministic case selection, loops, gotos,
31: variables, and the specification of correctness requirements.
32: The tool has fast algorithms for analyzing arbitrary
33: liveness and safety conditions.
34: .PP
35: Given a model system specified in
36: .SM PROMELA2\c
37: ,
38: .I spin
39: can perform interactive, guided, or random simulations
40: of the system's execution
41: or it can generate a C program that performs an exhaustive
42: or approximate verification of the system.
43: The verifier can check, for instance, if user specified system
44: invariants are violated during a protocol's execution, or
45: if non-progress execution cycles exist.
46: .PP
47: Without any options the program performs a random simulation of the system
48: defined in the input
49: .IR file ,
50: default standard input.
51: The option
52: .BI -n N
53: sets the random seed to the integer value
54: .IR N .
55: .PP
56: The group of options
57: .B -pglmrsv
58: is used to set the level of information reported
59: about the simulation run.
60: Every line of output normally contains a reference to the source
61: line in the specification that caused it.
62: .TP
63: .B p
64: Show at each time step which process changed state and what source
65: statement was executed.
66: .TP
67: .B l
68: In combination with option
69: .BR p ,
70: show the current value of local variables of the process.
71: .TP
72: .B g
73: Show the value of global variables at each time step.
74: .TP
75: .B r
76: Show all message-receive events, giving
77: the name and number of the receiving process
78: and the corresponding source line number.
79: For each message parameter, show
80: the message type and the message channel number and name.
81: .TP
82: .B s
83: Show all message-send events.
84: .TP
85: .B m
86: Ordinarily, a send action will be delayed if the
87: target message buffer if full.
88: With this option a message sent to a full buffer is lost.
89: The option can be combined with
90: .B -a
91: (see below).
92: .TP
93: .B v
94: Verbose mode: add extra detail and include more warnings.
95: .TP
96: .BI i
97: Perform an interactive simulation.
98: .TP
99: .B a
100: Generate a protocol-specific verifier.
101: The output is written into a set of C files, named
102: .BR pan. [ cbhmt ],
103: that can be compiled
104: .RB ( "cc pan.c" )
105: to produce an executable verifier.
106: Systems that require more memory than available
107: on the target machine can still be analyzed by compiling
108: the verifier with a bit state space:
109: .IP
110: .B " cc -DBITSTATE pan.c
111: .IP
112: This collapses the state space to 1 bit per system state,
113: with minimal side-effects.
114: Partial order reduction rules take effect during the
115: verification if the compiler directive
116: .B -DREDUCE
117: is used.
118: .IP
119: The compiled verifiers have their own sets of options,
120: which can be seen by running them with option
121: .BR -? .
122: .TP
123: .B t
124: If the verifier finds a violation of a correctness property,
125: it writes an error trail.
126: The trail can be inspected in detail by invoking
127: .I spin
128: with the
129: .B -t
130: option.
131: In combination with the options
132: .BR pglrsv ,
133: different views of the error sequence are then be obtained.
134: .TP
135: .B D
136: Perform a static dataflow analysis.
137: .TP
138: .B V
139: Print the version number and exit.
140: .SH SEE ALSO
141: G.J. Holzmann,
142: .I
143: Design and Validation of Computer Protocols,
144: Prentice Hall, 1991.
145: .br
146: \(em, ``Using
147: .SM SPIN\c
148: \&''.
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.