The following is a preliminary announcement for a first workshop on the use of SPIN that is being organized by Jean Charles Gregoire from INRS. Reactions and suggestions welcome!
October 16th, Montreal, QC (just before FORTE'95)
SPIN is a reachability analysis tool designed for the general verification of distributed systems. First made available publicly in 1991, a completely new version has recently been released. SPIN is used both for teaching and for industrial applications. It has inspired many other tools in various ways.
This workshop aims at bringing together the community of users and researchers interested in SPIN as a tool, as well as an experimentation or a research vehicle. It will be an opportunity to discuss the current status of the tool, and the evolution of SPIN.
We have identified the following areas of interest for this workshop:
Further suggestions are most welcome.
Participants are invited to present a position statement
to be presented and discussed at the workshop.
Workshop Organizer: INRS-Te'le'communications All Correspondance: gregoire@inrs-telecom.uquebec.ca
One More New Feature: Interactive Simulation
Following the request of many SPIN users, and the example of Patrice Godefroid, who made an initial implementation of interactive simulation long ago in his sleep-set extension of SPIN version 1.6, SPIN version 2.2 now has full support for interactive simulation.
Normally in a random simulation all nondeterminism is resolved with the help of a builtin pseudo random number generator. To make runs reproducible, so far the only option was to fix the seed of the random number generator with the -n option, but the specific way in which nondeterminism is being resolved is always unpredictable this way.
When the new version of SPIN is invoked as ``spin -i'' the user will be prompted for a choice whenever nondeterminism has to be resolved. The user can now directly guide a simulation run towards a particularly interesting, or suspect, piece of the code.
Interactive simulation is also supported from within XSPIN. When using XSPIN, a button menu will appear whenever a user selection is required.
Similar functionality existed for a long time in other
verification tools - so this does seem to fill a gap in
SPIN's functionality so far.
Other Recent Changes
The current version of SPIN is 2.2.6 from March 21 1995.
Apart from the extension of functionality related to the
implementation of interactive simulation, not much changed.
A series of small bug fixes was again made - a new, optional
compiler directive -DREACH was added - by request, support
for the binary exclusive-or operator ('^') was added
(the normal binary-or operator ('|') was already supported).
More details on all updates is always available in the
standard SPIN distribution file Doc/V2.Updates.
Some Frequently Asked Questions
Based on a new efficient algorithm from Doron Peled, Rob Gerth, Pierre Wolper, and Moshe Vardi, we now have a full implementation of a good translator that takes arbitrary LTL formulae as input, and produces the equivalent never claim, complete with the required labeling of acceptance states. It was already known that the size of the never claim (i.e., Buchi Automaton) is, in the worst case, exponential in the number of temporal operators in the the LTL formula. In practice, though, one rarely uses (or understands!) a formula with more than 2 or 3 operators, so this appears to be not much of a problem. We hope to be able to integrate the new algorithm into SPIN later - so that we can extend the Promela syntax with linear time temporal logic itself... Instead of a never claim, one could then specify the correctness claims directly as LTL formulae. (SPIN version 3?) Stay tuned.
Also a question that is asked a lot. Unfortunately we
do not know of a good method to implement CTL model
checking in an on-the-fly algorithm. Some methods have
been suggested, but they do not seem to be a clear win.
Also, we do not know of good examples of CTL formulae
that cannot be expressed equally well in (perhaps several)
LTL formulae. This is a point of debate though, and
your suggestions are welcome on this or any other point!
Appendix: Porting SPIN to DOS
The following report is from Prof. Michael J. Ferguson Email: mike@vimy.inrs-telecom.uquebec.ca and included here with his permission: It describes a successful attempt to port SPIN to a notebook PC - running under DOS. Many other SPIN users have asked about the possibility of this.
--- I have just successfully ported SPIN to my 486 PC subnotebook --- not without a few trials. Some details: ** Compiler ---Djgpp (GCC 2.6.3) ** Spin problems ... -- y.out.c and y.out.h are illegal DOS file names --- Bison (DOS) produces spin_tab.c and spin_tab.h --- all the y.out.h includes needed modifying. -- The linker would not produce an output file with multiple definitions of malloc, realmalloc, and free. I renamed malloc to smalloc in pangen1.h and its prototype in pangen3.h -- The "tmp" file could not be created. gcc usually inputs path names in unix format, and converts them, at some low level (I think) to DOS comaptible paths. Here it seemed to be interpreted with respect to the current path. Since spin uses only one temprorary file, I was able to hardwire one in. It also appears that the file is unlinked too soon. I removed the unlink.. with it there I obtained a "parse error in line 1: hello" This does not seem to be a problem on unix? ** gcc problems ... gcc has several incompatible prototypes in its library atoi(const char*) to atoi(char*) time(unsigned long*) to time(long*) extern void *(alloca) (long unsigned) to extern void *(alloca) (unsigned) tempnam(const char*, const char*) to tempnam(char*, char*) It runs well on my 486 subnotebook but not on my 386 (no 387) desktop. I am not certain why. Now I have to get some more memory for my subnote. Michael ---
Gerard J. Holzmann (gerard@research.bell-labs.com)