SPIN Verifier's Roadmap: iSpin


The easiest way to get started with 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 runs Spin in the background to obtain the desired output, and wherever possible it will attempt to generate a graphical representation of such 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 Roadmap.html.
This description assumes that the appropriate software has been installed on your system and that all relevant commands (such as wish, Spin, iSpin, and a C compiler such as gcc) are within your search path. If this is not the case, check the README file first.


To start a first session with iSpin, use one of the example Promela specifications from the Examples directory of the Spin distribution. For instance: The dollar 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: All further commands executed in the background, prompted by user selections in the other windows, will appear here as well.


You should now have the main Spin 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. Select one of the topics, and simply close the 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 the file being edited explicitly after changes; and then to select ReOpen from the top menu bar to read in the new version.


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 spec 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, where you can select simulation parameters for a simulation run. For now, just accept the default settings that are shown, and press the Run button, to perform a first simulation run.


A Message Sequence Chart will be created in the right panel (assuming your model includes message passing operations of course). The lower panels, labeled Data Values and Queues maintain the current values of all variables and channels used during the simulation run. For very large models, you may want to turn off data value tracking, if it starts slowing down a simulation run.
The simulation output 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.


Note that a log window at the upper right shows precisely which commands are generated by iSpin to let the main Spin tool perform the desired simulation. For instance: 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 not need for great concern about using Spin without this interface. You can find out what all the option flags to Spin mean by typing in a regular shell window: "spin --".)


By clicking in the boxes in the Message Sequence Chart displayed on the right the text window on the left should move to the corresponding points in the code.
Simularly, clicking on any filename:linenumber reference should bring up the corresponding file, positioned at the linenumber given.


Next, move to the Verification tab. There are again lots of choices that can be made about the type of verification that can be done. The most common choices are on the left side in light blue. The less frequently used, more advanced options are to the right in grey. Accept the default settings of the parameters and press the Run button.

The commands that iSpin generates are printed in the log, which is now in the right-hand side panel. Spin first generates a verifier, then compiles and executes it, and shows the results. If all is well, the results show that there are no errors 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, only a safety verification is performed. To check one of the LTL properties select Liveness acceptance cycles and provide the name of the ltl claim to be verified in the box just above the Run button, for instance property p0 or p1.


Introduce an artificial error in the specification by adding an statement (don't forget the semi-colon) immediately following either one of the occurrences of: becomes: Save the file (you have to move to the Edit/View panel to do that), and repeat the verification run.

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 in the assertion violation.


Bring up the Swarm Run panel. If you have swarm installed (if not, see http://spinroot.com/swarm) you can now easily setup a swarm run, using as many CPU cores as you have available. (This option will become more attractive as standard PCs start getting more and more CPU cores.) Don't select more cores than you actually have on your system and don't select more memory than you actually 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.


The final two tabs are to save or restore an entire verification session, including all options selects and intermediate results created. 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.

Spin HomePage (Page Updated: 4 May 2014)