1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
|
<html>
<head>
<title>Getting Started: Using iSpin</title>
<style type="text/css">
body {
font-family: Arial, Helvetica, sens-serif ;
}
.boxed {
margin-left: 24px ;
margin-right: 24px ;
margin-top: 12px ;
margin-bottom: 12px ;
padding-top: 12px ;
padding-left: 12px ;
padding-right: 12px ;
border: 1px solid blue ;
}
</style>
</head>
<body bgcolor=#ffffff>
<p>
<table width=100%><tr><td width=10%> </td><td>
<h1><tt>Getting Started:<br><font color=red>Using <i>iSPIN</i></font></tt></h1>
A convenient way to get started with routine use of <i>Spin</i> is to
use the graphical interface <i>iSpin</i>.
The graphical interface runs independently
from <i>Spin</i> itself, and helps by generating the proper
<i>Spin</i> commands based on menu selections.
<i>iSpin</i> invoked <i>Spin</i> itself in the background to obtain
the desired output, and wherever possible it will attempt to generate
a graphical representation of that output.
<i>iSpin</i> knows when and how to compile code for the
model checkers that <i>Spin</i> can generate, and it knows
when and how to execute it, so there is less to remember.
For more information on running <i>Spin</i> directly,
see the companion document <a href="Spin_Verification.html">Spin_Verification.html</a>,
and to get familiar with it, try the exercises in
<a href="Spin_Exercises.html">Spin_Exercises.html</a>.
<p>
The description below assumes that the appropriate software packages
(<tt>spin</tt>, <tt>ispin</tt>, <tt>wish</tt> for tcl/tk support,
optionally the <tt>dot</tt> tool from the GraphViz distribution,
and a standard C compiler such as <tt>gcc</tt>)
have been installed on your system and that all
relevant commands are within your search path.
If this is not the case, follow the instructions in the
<a href="http://spinroot.com/spin/Man/README.html">README</a> file first.
<h2><tt><font color=blue>One</font></tt></h2>
To start a first session with <i>iSpin</i>,
use one of the example <i>Promela</i> specifications
from the <i>Examples</i> directory of the <i>Spin</i> distribution.
For instance:
<ul>
<pre>$ cd Examples/LTL
$ ispin leader.pml
</pre>
</ul>
The dollar sign above (<tt>$</tt>) is the prompt of the command-shell.
The next two words are typed by the user.
If all is well, after ispin starts up it will print something
like the following in its command-log at the bottom of the
main window:
<ul>
<pre>
SPIN LOG:
Spin Version 6.3.0 -- 4 May 2014
iSpin Version 1.1.1 -- 22 February 2014
TclTk Version 8.5/8.5
1 leader.pml:1
</pre>
</ul>
All further commands executed in the background, prompted by
user selections in the other windows, appear here as well.
<h2><tt><font color=blue>Two</font></tt></h2>
You should now have the main <i>iSpin</i> control window on the
display, with a <i>Promela</i> specification of the leader election
protocol loaded.
First, press the <b>Help</b> button in the top menu bar
to view the available help topics. Browse some of the topics,
and close the Help window when done.
<p>
The main text window on the left offers some basic
edit and search capabilities. You can scroll through the
specification either with button-2 down (on a 3-button mouse),
or with the scroll-bar.
<p>
You can select text fragments by sweeping the mouse with
button-1 (the left-most button) down. Control-C (copy),
Control-V (past), and Control-Z (undo) are supported.
If you are more comfortable working with another text-editor,
a reasonable way of working with <i>iSpin</i> is also to have the text
of a specification open in your favorite editor.
To update <i>iSpin</i>'s view of the file after externally editing it,
select <b>ReOpen</b> from the top menu bar.
<h2><tt><font color=blue>Three</font></tt></h2>
Still within this first view, you can perform a basic <b>Syntax Check</b>,
and a basic check for <b>Redundancies</b>, by selecting the corresponding
buttons near the top of the screen. You can also get the <b>Symbol
table</b> of the Promela specification printed out in the same way.
<p>
The <b>Automata View</b> panel on the right hand side of the screen relies
on the availability of the <b>dot tool</b> from the graphviz distribution.
If you have it installed, clicking on the automata view button can
display each proctype as a graph.
<p>
Next, move to the <b>Simulate/Replay</b> tab, at the top-left of the display.
This allows you to select a range of parameters for a simulation run.
For now, just accept the default settings that are
shown, and press the <b>Run</b> button, on the right, to perform a
first simulation run.
<h2><tt><font color=blue>Four</font></tt></h2>
A <i>Message Sequence Chart</i> will be created in the right mid-panel
(assuming your model includes message passing operations of course).
Resize it to suit your needs.
<p>
The panels on the bottom of the screen contain additional information about
the run.
The lower-left and lower-right display the current <b>Data Values</b> and
<b>Channel Contents</b> respectively, at each point in the run.
For very large models, you may want to turn off data value tracking,
if it starts slowing down the simulations.
<p>
The simulation output itself appears in the middle panel at the bottom.
Once a run is completed, or stopped, you can use the Rewind button
to go back to the start of the run, and step forwards or backwards
through it -- with all values and queue states updated appropriately.
You can also click in the message sequence chart or the output panel
to move to a specific point in the run.
<h2><tt><font color=blue>Five</font></tt></h2>
A log window at the upper right of the <i>iSpin</i> display
shows which commands are being generated by iSpin and executed
by <i>Spin</i> in the background.
For instance, the simulation run will probably be invoked as follows:
<ul>
<pre>
spin -X -p -v -g -l -s -r -n1 -j0 leader.pml
</pre>
</ul>
The advantage of using <i>iSpin</i> is that you
do not have to remember the meaning of all the options that
<i>Spin</i> recognizes. (Not all the the options used above are
critical though, so there's also no need for concern if
you rather use <i>Spin</i> without this interface.
You can find out what all the options to <i>Spin</i> are
by typing in a regular shell window: "<tt>spin --</tt>"
<h2><tt><font color=blue>Six</font></tt></h2>
By clicking in the boxes in the <i>Message
Sequence Chart</i> displayed on the right, the text
window with the <i>Spin</i> model on the middle left
should move to the corresponding point in the code.
<!--
Simularly, clicking on any filename:linenumber reference should bring
up the corresponding file, positioned at the linenumber given.
-->
<h2><tt><font color=blue>Seven</font></tt></h2>
Next, move to the tab labeled <b>Verification</b> in the top menu bar.
There are lots of choices that can be made about the type of verification
that can be done. The most common choices are in the panels
at the top left, colored light blue.
The less frequently used, and more advanced options can be displayed by
clicking the black option buttons titled <b>Show...</b> to the right.
For now, accept the default settings of the parameters and press the <b>Run</b>
button near the middle of the display.
<p>
The commands that <i>iSpin</i> generates are printed in the log,
which is now shown in the black right-hand side panel.
<i>iSpin</i> first generates a verifier, then compiles and executes it, and
shows the results. If all is well, no errors are detected in the specification.
The version of the leader election protocol that is being verified
contains several correctness requirements specified as inline LTL formula.
<p>
By default, <i>iSpin</i> is setup to perform a safety verification only.
To check one of the LTL properties, select under <b>Liveness</b> (left side
of the screen, in light blue), the option <b>acceptance cycles</b>
and type the name of the LTL property to be verified in the box just
above the <b>Run</b> and <b>Stop</b> buttons.
For instance, type <tt>p0</tt>, <tt>p1</tt>, <tt>p2</tt>, or <tt>p3</tt>.
<h2><tt><font color=blue>Eight</font></tt></h2>
Introduce an artificial error in the specification by adding an
<ul>
<pre>
assert(false)
</pre>
</ul>
statement on line 27, as follows:
<ul>
<pre>
:: Active ->
</pre>
</ul>
becomes:
<ul>
<pre>
:: Active -> assert(false)
</pre>
</ul>
<b>Save</b> the file (you have to move to the <b>Edit/View</b> panel to do that),
and repeat the verification by clicking the <b>Run</b> button.
<p>
This time, the verification should come back with an error
sequence, and notice at the bottom of the output window recommends
to replay the error trail from the <b>Simulate/Replay</b> panel.
Bring up that tab and make sure a <b>Guided</b> simulation is selected.
(A guided simulation can only be done for an error sequence
that was produced earlier by the verifier.)
Perform the guided simulation, which will now replay the error sequence
found, ending with the assertion violation.
<h2><tt><font color=blue>Nine</font></tt></h2>
<i>For advanced use.</i>
Bring up the <b>Swarm Run</b> panel. If you have <tt>swarm</tt> installed
(if not, see <a href="http://spinroot.com/swarm">http://spinroot.com/swarm</a>),
and you have a multi-core computer with a reasonable number of CPU cores,
you can now setup a swarm run, using as many cores as you have available.
<ul>
<i>Note: This option will become more attractive as standard PCs start
getting more and more CPU cores.</i>
</ul>
Don't select more cores than you physically
have on your system and don't select more memory than you
have. The options in the top right-panel show how <i>Spin</i>
will compile the verifier to create lots of different types of
verification runs. This method is especially useful for very
large verification models that cannot be exhaustively verified,
but where we still want to gain maximum confidence that we can
find the errors in a reasonable amount of time.
<h2><tt><font color=blue>Ten</font></tt></h2>
The final two tabs at the top of the <i>iSpin</i> display
are to <b>Save</b> or <b>Restore</b> an entire verification
session, including all options selected and intermediate results
created. It can be useful to remember what precisely you did and how you
found counter-examples. It provides a small approximation of a
version management system for <i>Spin</i> verification runs.
<br>
The very last button in the top menu ribbon is <b>Quit</b>,
but why would you ever want to do that?
<p><p><p><hr>
<table cols=3 width=100%>
<tr>
<td valign=top>
<a href="http://spinroot.com/spin/">Spin HomePage</a>
</td>
<td valign=top align=center></td>
<td valign=top align=right>
<font size="3"><b><tt>(Page Updated: 8 May 2014)</tt></font></b></td></tr>
</table>
</td><td width=15%> </td></tr></table>
</html>
|
