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 defined a simple
extension of LTL that gives it the full expressive power of omega
regular properties, matching that of never claims in Spin.
Spin Version 3.3.10
corrects a number of flaws in the basic LTL conversion that were
found by Heikki Tauriainen [email protected]. 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 [email protected] 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 [email protected] 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.