![[BACK]](/cvsweb/icons/back.gif){kind=icon}
Return to spin.1 CVS log ![[TXT]](/cvsweb/icons/text.gif){kind=icon}
![[DIR]](/cvsweb/icons/dir.gif){kind=icon}
Up to [Research Unix] / researchv10dc / vol2 / spin|
Return to spin.1 CVS log | Up to [Research Unix] / researchv10dc / vol2 / spin |
1.1 root 1: .TH SPIN 1
2: .CT 1 comm_mach protocol
3: .SH NAME
4: spin \(mi protocol analysis software
5: .SH SYNOPSIS
6: .B spin
7: [
8: .BI -n N
9: ]
10: [
11: .BI -pfglpqrsm
12: ]
13: [
14: .BI -at
15: ]
16: [
17: .I file
18: ]
19: .SH DESCRIPTION
20: .I Spin
21: is a tool for analyzing the logical consistency of
22: concurrent systems, specifically communication protocols.
23: The system is specified in a guarded command language called Promela.
24: The language, described in the reference,
25: allows for the dynamic creation of processes,
26: nondeterministic case selection, loops, gotos,
27: variables and assertions.
28: The tool has fast and frugal algorithms for analyzing
29: liveness and safeness conditions.
30: .PP
31: Given a model system specified in Promela,
32: .I spin
33: can either perform random simulations of the system's execution
34: or it can generate a C program that performs a fast exhaustive
35: validation of the system state space.
36: The validator can check, for instance, if user specified system
37: invariants may be violated during a protocol's execution, or
38: if any non-progress execution cycles exist.
39: .PP
40: Without any options the program performs a random simulation.
41: With option
42: .TP
43: .BI -n N
44: the seed for the simulation is set explicitly to the integer value
45: .BR N .
46: .PP
47: A second group of options
48: .B -pglrs
49: is used to set the desired level of information that the user wants
50: about the simulation run.
51: Every line of output normally contains a reference to the source
52: line in the specification that caused it.
53: .TP
54: .B p
55: Show at each time step which process changed state.
56: .TP
57: .B l
58: In combination with option
59: .BR p ,
60: show the current value of local variables of the process.
61: .TP
62: .B g
63: Show at each time step the current value of global variables.
64: .TP
65: .B r
66: Show all message-receive events, giving
67: the name and number of the receiving process
68: and the corresponding the source line number.
69: For each message parameter, show
70: the message type and the message channel number and name.
71: .TP
72: .B s
73: Show all message-send events.
74: .PP
75: Two options can be used to alter the model definition itself.
76: .TP
77: .B m
78: Changes the semantics of send events.
79: Ordinarily, a send action will be delayed if the
80: target message buffer if full.
81: With this option a message sent to a full buffer is lost.
82: The option can be combined with
83: .TP
84: .B q
85: Causes spin to inspect the Promela code for sequences that
86: can safely be cast into atomic sequences, to allow a
87: reduction of the complexity of larger validation runs.
88: Manual placement of atomic sequences can usually achieve
89: still larger reductions.
90: .B -a
91: (see below).
92: .TP
93: .B a
94: Generate a protocol-specific analyzer.
95: The output is written into a set of C files, named
96: .BR pan. [ cbhmt ],
97: that can be compiled
98: .RB ( "cc pan.c" )
99: to produce an executable analyzer.
100: Large systems, that require more memory than available
101: on the target machine, can still be analyzed by compiling
102: the analyzer with a bit state space:
103: .IP
104: .B cc -DBITSTATE pan.c
105: .IP
106: This collapses the state space to 1 bit per system state,
107: with minimal side-effects.
108: .IP
109: A compiled analyzer has its own set of options,
110: which can be seen by typing
111: .BR "a.out -?" .
112: .TP
113: .B t
114: If the analyzer finds a violation of an assertion, a deadlock,
115: a non-progress loop, or
116: an unspecified reception, it writes an error trail into a file
117: named
118: .BR pan.trail .
119: The trail can be inspected in detail by invoking
120: .I spin
121: with the
122: .B t
123: option.
124: In combination with the options
125: .B pglrs
126: different views of the error sequence are then easily obtained.
127: .SH SEE ALSO
128: .I cospan
129: in
130: .IR langs (1)
131: .br
132: G.J. Holzmann,
133: `Spin \(em A Protocol Analyzer',
134: this manual, Volume 2.
This archive runs on limited infrastructure. Preserving old code on modern bandwidth. Automated agents are requested to crawl responsibly.