| |
Getting Started:
Using iSPIN
A convenient way to get started with routine use of Spin is to
use the graphical interface iSpin.
The graphical interface runs independently
from Spin itself, and helps by generating the proper
Spin commands based on menu selections.
iSpin invoked Spin itself in the background to obtain
the desired output, and wherever possible it will attempt to generate
a graphical representation of that output.
iSpin knows when and how to compile code for the
model checkers that Spin can generate, and it knows
when and how to execute it, so there is less to remember.
For more information on running Spin directly,
see the companion document Spin_Verification.html,
and to get familiar with it, try the exercises in
Spin_Exercises.html.
The description below assumes that the appropriate software packages
(spin, ispin, wish for tcl/tk support,
optionally the dot tool from the GraphViz distribution,
and a standard C compiler such as gcc)
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
README file first.
One
To start a first session with iSpin,
use one of the example Promela specifications
from the Examples directory of the Spin distribution.
For instance:
$ cd Examples/LTL
$ ispin leader.pml
The dollar sign above ($) 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:
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
All further commands executed in the background, prompted by
user selections in the other windows, appear here as well.
Two
You should now have the main iSpin control window on the
display, with a Promela specification of the leader election
protocol loaded.
First, press the Help button in the top menu bar
to view the available help topics. Browse some of the topics,
and close the Help window when done.
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.
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 iSpin is also to have the text
of a specification open in your favorite editor.
To update iSpin's view of the file after externally editing it,
select ReOpen from the top menu bar.
Three
Still within this first view, you can perform a basic Syntax Check,
and a basic check for Redundancies, by selecting the corresponding
buttons near the top of the screen. You can also get the Symbol
table of the Promela specification printed out in the same way.
The Automata View panel on the right hand side of the screen relies
on the availability of the dot tool from the graphviz distribution.
If you have it installed, clicking on the automata view button can
display each proctype as a graph.
Next, move to the Simulate/Replay 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 Run button, on the right, to perform a
first simulation run.
Four
A Message Sequence Chart will be created in the right mid-panel
(assuming your model includes message passing operations of course).
Resize it to suit your needs.
The panels on the bottom of the screen contain additional information about
the run.
The lower-left and lower-right display the current Data Values and
Channel Contents 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.
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.
Five
A log window at the upper right of the iSpin display
shows which commands are being generated by iSpin and executed
by Spin in the background.
For instance, the simulation run will probably be invoked as follows:
spin -X -p -v -g -l -s -r -n1 -j0 leader.pml
The advantage of using iSpin is that you
do not have to remember the meaning of all the options that
Spin recognizes. (Not all the the options used above are
critical though, so there's also no need for concern if
you rather use Spin without this interface.
You can find out what all the options to Spin are
by typing in a regular shell window: "spin --"
Six
By clicking in the boxes in the Message
Sequence Chart displayed on the right, the text
window with the Spin model on the middle left
should move to the corresponding point in the code.
Seven
Next, move to the tab labeled Verification 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 Show... to the right.
For now, accept the default settings of the parameters and press the Run
button near the middle of the display.
The commands that iSpin generates are printed in the log,
which is now shown in the black right-hand side panel.
iSpin 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.
By default, iSpin is setup to perform a safety verification only.
To check one of the LTL properties, select under Liveness (left side
of the screen, in light blue), the option acceptance cycles
and type the name of the LTL property to be verified in the box just
above the Run and Stop buttons.
For instance, type p0, p1, p2, or p3.
Eight
Introduce an artificial error in the specification by adding an
assert(false)
statement on line 27, as follows:
:: Active ->
becomes:
:: Active -> assert(false)
Save the file (you have to move to the Edit/View panel to do that),
and repeat the verification by clicking the Run button.
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 Simulate/Replay panel.
Bring up that tab and make sure a Guided 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.
Nine
For advanced use.
Bring up the Swarm Run panel. If you have swarm installed
(if not, see http://spinroot.com/swarm),
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.
Note: This option will become more attractive as standard PCs start
getting more and more CPU cores.
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 Spin
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.
Ten
The final two tabs at the top of the iSpin display
are to Save or Restore 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 Spin verification runs.
The very last button in the top menu ribbon is Quit,
but why would you ever want to do that?
| |