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
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).
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 (email@example.com). We'll send out more details as they become available.
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.
spin -p -r -s -P/usr/gerard/bin/cpp promela_specwill 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.
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 firstname.lastname@example.org for inclusion in one of the upcoming Newsletters.
Gerard J. Holzmann (email@example.com)