NewsLetter 28 - March 17, 2000:
Spin2000 Workshop Update
SPIN2000 will span three consecutive days. Each of the workshop days will start with a keynote speech. We are very pleased to announce the following three invited speakers:
Leslie Lamport, Compaq Research Center.
Author of a number of seminal papers on the verification of concurrent systems, starting in the mid seventies. One of the true pioneers of our field. Lamport will share his experiences with the construction of a new model checking tool for TLA.
Bill Roscoe, Oxford University Computing Laboratory.
One of the lead people involved with the design and implementation of the FDR model checker, one of the first such systems to be marketed commercially.
Peter Gluck, NASA's Jet Propulsion Laboratory.
Software lead for the recent Deep-Space 1 mission, and participating in NASA's ongoing Cassini mission to Saturn.
The deadline for submissions, and proposals for tutorials and tool demonstrations, to is May 1, 2000. For the latest details on the workshop please see the workshop homepage:
SPIN2000 takes place in the week before the FMOODS conference: the IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems, which occurs September 6-8 at the location. For details please see:
SPIN2001: We are also looking for proposals for the organization of next year's SPIN workshop. If you're interested please send a note to any one of the Spin2000 organizers.
SPIN Version 3.3.10
Spin Version 3.3.10 includes some improvements in the generation of never claims (Buchi Automata) from LTL formulae, that were mostly inspired by the work of Kousha Etessami kousha@research.bell-labs.com. Kousha defined a simple extension of LTL that gives it the full expressive power of omega regular properties, matching that of never claims in Spin. Kousha's conversion, and an explanation of the formalism, is available via URL: http://cm.bell-labs.com/cm/cs/what/spin/eqltl.html
Spin Version 3.3.10 corrects a number of flaws in the basic LTL conversion that were found by Heikki Tauriainen htauriai@cc.hut.fi. Heikki has developed a random testing method for LTL conversion algorithms that works remarkably well. If the new version of Spin is more robust, this is largely due to Heikki's excellent work.
Version 3.3.10 contains a small extension that makes it easier to model function calls in some common cases. Version 3.3.10 allows the use of the predefined variable _nr_pr, that holds the number of currently executing processes. One can start a process and wait its completion by writing: "p = run fct_call(parameters); (_nr_pr == p);". The run statement returns the value of _nr_pr at the time of the call, while _nr_pr itself is incremented by one. When the newly instantiated process completes and is removed from the state-vector _nr_pr is decremented again and returns to its old value. Beware, however, that processes are removed from the state-vector in last-in-first-out order.
Appendices
The URL: http: //www.abo.fi/~iporres/vUML/ describes a new UML-based tool that uses SPIN as its verification engine.
Two announcements:
From: Radu Iosif iosif@athena.polito.it
This message announces the release of dSPIN 3.2.0+0.2. It is still compliant with SPIN 3.2.0 (no upgrade to 3.3.10 yet). In addition to the old version (called simply dSPIN 3.2.0) it includes garbage collection features. Two classic GC algorithms are implemented: "reference counting" and "mark and sweep". Collection algorithms can be switched on and off with macro definitions (-DGC0 for reference counting, -DGC1 for mark and sweep). For more details and download visit: http://www.dai-arc.polito.it/dai-arc/auto/tools/tool7.shtml
From: Michal Pakula mpakula@mimuw.edu.pl
I study at Institute of Informatics, Warsaw University and I a few months ago I started working on my master thesis. It concerns translation of Estelle specifications to a language which helps formal verification. So my first step was to find a target language and Promela looks quite perfect for me. But before I go deep in it I'd like to find out weather you know anything about this kind of project going on or done somewhere in the world (I mean translation of Estelle specifications to Promela). I'd be grateful for help. -- Michal Pakula
End of Newsletter Nr. 28.
Spin Homepage, spin_list@research.bell-labs.com