SPIN NEWSLETTER Nr. 19

`Contents NewsLetter 19 - August 12, 1997:`

The New Spin Version 3.0 Online Man-Pages for Promela and Spin Some Interesting URLs: PEP's link with Spin The VIRES Project DIMACS Volume Published Recent Papers

`The New Spin Version 3.0`

The last Spin update was made about four months ago. Since then, we have been working hard on a new release of the software with some interesting new features. The new functionality is described in the updated version of WhatsNew.ps, but a brief summary of the main points follows here. Thanks to Rob Gerth, Anuj Puri, Michael Ferguson, Erich Mikk, Bart Knaack, Doron Peled, Margaret Redberg, and Pamela Zave for providing feedback on the alpha release over the last few months. Thanks also to Klaus Havelund and Frank Schneider for suggesting many improvements.

Version 3.0 adds event trace definitions to Promela. Event traces allow one to state properties of a system in terms of event occurrences, rather than purely in terms of states (the default in Spin). This makes it possible, for instance, to make correctness claims about arbitrary send and receive events, including rendezvous (hard to do with never claims).
Version 3.0 contains a new BDD-like state compression option that is based on the storage of reachable states with the help of a minimized automaton representation. The work was inspired by the studies of Willem Visser (cs.man.ac.uk!visserw) and Jean-Charles Grégoire (inrs-telecom.uquebec.ca!gregoire) on state compression, reported at the Spin96 and Spin97 workshops. The algorithm for the minimized automaton representation is by Anuj Puri (anuj@research.bell-labs.com), and described in an upcoming paper. As reported earlier by Grégoire, memory reduction of one to two orders of magnitude over standard verification runs are feasible with these methods, in return for an increase of run times.
There are several new lines of development that have opened up with the minimized automaton representation of the state space. One is a potential for the addition of symbolic model checking capabilities to Spin. Another option, that is already part of Version 3.0, is a simple checkpoint/recovery scheme for verification runs that use the minimized automaton representation. Every one million states a checkpoint file can be created, and if the run is aborted for any reason, it can be restarted from one of those checkpoint files without loss of continuity.
There is a new columnated simulation output mode for Spin that mimicks the message flow view one could so far only obtain through the intermediacy of the Xspin graphical interface.
```
	Usage: spin -c spec
```
It can be considerably more informative than the standard tracebacks. Inspiration for this new feature (and for event traces) was a brief comparison of Spin with one of its early predecessors trace from 14 years ago. In this case, trace turned out to have some options that had been lost in the succession of tools.
Spin has a new Postscript output option for generating message flows as printable Postscript files.
```
	Usage: spin -M spec
	or:    spin -t -M spec
```
which produces the file spec.ps The second form above converts an error trail into Postscript.
Xspin now has an option to track not just message flows but also variable accesses inside MSC displays. It suffices to prefix a variable declaration with the new keyword show, e.g. show byte cnt;, and selecting the option Show Selected Variables in the Simulation Panel.
Also added was an automatic tracking of the state changes in a never claim in the MSCs during guided simulations (i.e., when inspecting an error.trail), to give more clues about the nature of an error. The never claim changes state whenever one moves from one term to another in an LTL formula.
The new Xspin 3.0.0 is compatible with both Windows95 and WindowsNT, and works with all current versions of Tcl/Tk (up to and including 8.0).
Some users have reported problems with the LTL conversion option in Spin, when they use a shell with non-standard quoting conventions. To prevent these problems, Spin version 3.0 has an extra option to retrieve an LTL formula from a file, instead of from the command line.
Usage: spin -f "[]p" or : spin -F file with: []p as the first line in 'file'

For an instant upgrade to Spin Version 3.0.0: http://netlib.bell-labs/netlib/spin/spin300.tar.gz
For the precompiled PC version: http://netlib.bell-labs/netlib/spin/pc_spin300.zip
Online Man-Pages for Promela and Spin
It is hard to keep the Spin documentation always up to date with recent changes. A start has been made with the construction of a web-site that contains all the relevant information about the language and the tool, combining information that has so far been scattered over different documents. These online references can be found at url: http://cm.bell-labs.com/cm/cs/what/spin/Man/index.html.
If you would rather store these pages on your local host, you can also download the complete set from: http://netlib.bell-labs/netlib/spin/html.tar.gz.
The online references will be kept up to date with future changes in the language and the toolset. Suggestions for extensions and improvement are most welcome.
PEP's link with Spin
The PEP tool (Programming Environment based on Petri Nets) is a toolset for the construction, simulation, and verification of Petri Nets. In it's last release it has gained an interface to Spin, to allow for LTL model checking of Petri Net models (with a builtin translation from Petri Nets to Promela.) The PEP URL is: http://www.informatik.uni-hildesheim.de/~pep/HomePage.
The VIRES Project
VIRES (Verifying Industrially Relevant Systems) is a collaborative research project of a number of leading universities in Europe (Eindhoven, Grenoble, Liege, Kiel). The following paragraphs are copied from the VIRES URL at http://www.win.tue.nl/cs/fm/vires/ (worth browsing further).
``Within VIRES a number of separate tools (Spin, Caesar/Aldbaran, Kronos, V-TOOL), each with their own model description language, are used. Nevertheless, the verification approaches of the VIRES tools are all based on the same basic automata-theoretical concepts. Accordingly, we shall define the protocol in a neutral language (e.g., communicating timed omega-automata) from which tool-specific model descriptions are derived by essentially syntactical rewriting.''
... ``To scale-up its verification tools, the VIRES project will need to investigate techniques both to make its tools more efficient, such as abstraction methods, as well as to extent their applicability to, e.g., the verification of time and duration properties.''

DIMACS Volume Published
With some delay, the proceedings of the 1996 Spin Workshop have finally been published as a nicely bound volume of 203 pgs titled The Spin Verification System. that can be ordered for $49 from the AMS as DIMACS Volume 32 (the price is lower for DIMACS members). See http://www.ams.org/bookstore/ and search on the word SPIN in a book-title.
The papers are the updated versions of the preprint papers that are still online as the workshop proceedings. The table of contents for the volume is:

Preface
J.-Ch. Grégoire -- State space compression with graph encoded sets
G. J. Holzmann and O. Kupferman -- Not checking for closure under stuttering
G. J. Holzmann, D. Peled, and M. Yannakakis -- On nested depth first search
H. E. Jensen, K. G. Larsen, and A. Skou -- Modelling and analysis of a collision avoidance protocol using Spin and Uppaal
P. Kars -- The application of Promela and Spin in the BOS project
S. Leue and P. B. Ladkin -- Implementing and verifying MSC specifications using Promela/XSpin
S. Löffler and A. Serhrouchni -- Creating implementations from Promela models
P. Merino and J.-M. Troya -- Modelling and verification of the MCS layer with Spin
E. Najm and F. Olsen -- Protocol verification with reactive Promela/Rspin
V. Natarajan and G. J. Holzmann -- Outline for an operational semantics of Promela
S. K. Shukla, D. J. Rosenkrantz, and S. S. Ravi -- A simulation and validation tool for self-stabilizing protocols
J. Tuya, J. R. de Diego, C. de la Riva, and J. A. Corrales -- Dynamic analysis of SA/RT models using Spin and modular verification
W. Visser and H. Barringer -- Memory efficient state storage in Spin

Recent Papers

Author: Michael J. Ferguson, INRS-Telecom.UQuebec.CA!mike Title: Formalization and Validation of the Radio Link Protocol (RLP1), Publication: Computer Networks, V29 N3, pp. 357-372. Contents: Discusses the validation of a radio link protocol (RLP1) with Spin, as part of the protocol's standardization. It is argued that a suite of accepted formal notations is necessary to formalize the many different parts of a protocol standard.

Author: Gerard Holzmann, gerard@research.bell-labs.com Title: The model checker Spin Publication: IEEE Trans. on Software Engineering, May 1997, V23 N5, pp. 279-295. Contents: The paper gives an overview of the design and structure of the verifier, reviews its theoretical foundation, and gives an overview of significant practical applications to date. Title: Designing Bug-Free Protocols with Spin Publication: Computer Communications Journal, March 1997, V20 N2, pp. 97-105. Contents: Outlines the use of Spin to address protocol design problems. As an example it considers the verification of a published protocol for implementing synchronous rendezvous operations in a distributed system.

End of Newsletter Nr. 19.

Spin (spin_list@research.bell-labs.com)

`Contents NewsLetter 19 - August 12, 1997:`

`The New Spin Version 3.0`

`Online Man-Pages for Promela and Spin`

`PEP's link with Spin`

`The VIRES Project`

`DIMACS Volume Published`

`Recent Papers`

End of Newsletter Nr. 19.