SPIN NEWSLETTER Nr. 18

Contents NewsLetter 18 - April 20, 1997:

Workshop Report
Online Proceedings
Tentative Plans for SPIN98
Recent Changes in Spin
Recent Papers

Workshop Report

The third Spin workshop, held 5 April at Twente University, in the Netherlands, attracted 60 people (slightly up from last year's 50 participants). Pierre Wolper, from the University of Liege in Belgium, gave an inspiring keynote presentation, followed by 11 other speakers. Roughly half of the presentations focused on applications of the Spin model checker to practical problems, the other half focused on foundational issues. One of the scheduled speakers, Dr. Tadashi Nakatani from Toshiba Corp. in Japan, was alas unable to attend. Two other speakers could step in to give short presentations on their work: Bart Knaack from the University of Eindhoven (speaking on work towards an alternative real-time extension of Spin), and Pieter Villiers from the University of Stellenbosch in South Africa (speaking on his work on a different model checker that can be compared with Spin).

Online Proceedings

An online version of the proceedings of SPIN97, including all papers, as well as the viewgraphs of Pierre Wolper's keynote presentation, and Knaack, and Villiers' talks, can be found at: http://netlib.bell-labs.com/netlib/spin/ws97/papers.html. The abstracts contain the links to compressed postscript files for all papers or slides.
Proceedings from the previous workshops can also still be accessed online. (Replace "ws97" with "ws96" or "ws95" in the url above.)

Spin98

There's no time wasted in planning ahead. We have the tentative plan to organize next year's Spin Workshop in October 1998, following the next FORTE/PSTV conference, at ENST in Paris, France. If all goes as planned, the local workshop organizer will be Elie Najm (najm@res.enst.fr). We'll send out more details as they become available.

Recent Changes

Spin relies on the standard C preprocessor to process #define macros and #include files. The processor is conventionally named cpp and on Unix systems can be found in /lib/cpp (or in /usr/ccs/lib/cpp on Sun Solaris systems).
On Unix systems this works well enough that many users are not even aware that the preprocessing phase takes place. There are two cases where this can give some problems though.

Suppose you would like to extend the language, and define your own version of Promela++. It would be nice if you could specify a different preprocessor than the default. Perhaps you'd like to arrange it in such a way that your own preprocessor first performs some expansions for syntax you have added to the language, before passing the specification to cpp for processing.
On some PC's with Borland C++, instead of gnu cc, installed as the default C compiler, the command cpp actually invokes the full compiler (cpp here abbreviates c_plus_plus, instead of c_pre_processor...), with undesired results. In this case one would like to be able to tell Spin where the 'real' C preprocessor is.

To solve both problems, the current release of Spin, version 2.9.7. recognizes a new command-line option -Pxxx, with xxx the name of an executable program that will be used to process the Promela source before Spin itself tries to parse it. For instance, invoking Spin as:

	spin -p -r -s   -P/usr/gerard/bin/cpp   promela_spec

will invoke spin in simulation mode (using the first three options), but invoke a private preprocessor in /usr/gerard/bin/cpp instead of the default /lib/cpp.
On PC's it is simple enough to change the template for the call to the spin executable, at the start of the xspin Tcl/Tk script, to invoke a different processor. The change should make it much simpler to construct Promela++ extensions without requiring surgery on the Spin default parser.
There are several other minor upgrades of Spin itself (see the Doc/V2.Updates file for details on these and all other updates). There is now a single Readme file, that should simplify the installation of Spin for new users. The other main improvement in the releases of Spin 2.9.5 and later is the improved Collapse compression mode, described in this year's workshop. If you haven't updated your version of Spin lately, now may be a good time. (Always update both Spin and Xspin at the same time. In some cases, Xspin will rely on changes made in the Spin code and vice versa.)

Overview Paper

An overview of the theoretical background of Spin, and a set of examples on the application of Spin to significant design problems, will appear in the IEEE Transactions on Software Engineering. The article is titled The Model Checker Spin, and is scheduled to appear in the upcoming special issue Formal Methods in Software Practice, edited by Prof. Laurie Dillon and Dr. Sriram Sankar, due out in May 1997.

If you have published a paper on work related to the Spin system, have spotted a paper that hasn't been mentioned here, or would like feedback on a draft paper from other Spin users, send the bibliographic reference, and/or a url reference, to spin_list@research.bell-labs.com for inclusion in one of the upcoming Newsletters.

End of Newsletter Nr. 18.

Gerard J. Holzmann (gerard@research.bell-labs.com)