Many have already signed up for the SPIN97 workshop in Twente two weeks from now. Registration and participation is free. To help plan for the right number of chairs and lunches, however, please send a note to Rom Langerak if you plan to come and have not yet send in a registration:
langerak@cs.utwente.nlThe keynote presentation at the SPIN97 workshop is by Pierre Wolper, together with Moshe Vardi responsible for defining the formal automata theoretic framework for verification that underlies Spin. Below is the abstract for Pierre's talk on April 5. We hope to see you all at the workshop!
Where could SPIN go next?
A unifying approach to exploring infinite state spaces
Pierre Wolper
University of Liege
Starting with the observation that many verification problems can be
reduced to deciding various forms of state reachability, this talk
then examines how the latter can be done in the context of infinite
state systems. It identifies the central problem to be solved as
computing, in a way that can generate an infinite number of states in
a finite amount of time, the fixpoint of the (forwards or backwards)
transition relation of the program to be analyzed. Doing this
requires three basic components: a finite representation for infinite
sets of states together with the algorithms for manipulating it; a
technique for bootstrapping from finite to infinite sets of states;
and a termination criterion. For the first component, its is shown
that regular sets play a central role. For the second, a variety of
techniques are discussed, but one, the "loop-first search", is
emphasized. For the third, it is argued that termination detection is
sufficient and that termination guarantee offers little additional
practical advantage beyond a theoretical illusory peace of mind.
The proceedings of the 1996 Spin Workshop are now listed on the home page of the AMS as Volume DIMACS/32 (i.e., not DIMACS/39 as we thought before). See http://www.ams.org/bookstore/ and follow the links for 'Books' and 'What's New'
The book is expected to be ready for shipping by early May (sadly, not in time to be available at this year's workshop.) The volume for the Partial Order Methods workshop (DIMACS/29) has been published and was said to be available by mid March.
There is a formal methods applications database at URL:
http://www.csr.ncl.ac.uk/projects/FME/InfRes/applications/index.html
If you have a significant application of Spin, you can consider
submitting the information for inclusion in this database. There is
a form available at the above URL. For more information contact
the maintainer of the database, Nico.Plat@ACM.org
The current version of Spin is 2.9.6. It has a thoroughly revised (and much improved) version of the Collapse compression mode, as promised in Newsl. 15 and described in the Spin97 workshop paper. Xspin has also been updated to work correctly with the last stable release of Tcl/Tk 7.6/4.2. (Be warned not to try it yet with the alpha releases 8.0, it's known to break.)
There is also a new version of the pc_spin296.zip file that contains a 32-bit executable. The new Tcl/Tk actually cares about this when you run Spin on the PC (the older versions can hang up your system during simulations.)
Il-Hyung Cho asks:
From cs.clemson.edu!ihcho Sun Mar 2 20:08:03 EST 1997
From: cs.clemson.edu!ihcho (Il-Hyung Cho)
Subject: API for SPIN?
Is there an API (Application Programming Interface) exists
for the SPIN tool? Does SPIN provide an interface that my
C++ or Java program can work with?
If anyone has written such an API, please send us a note.
Some interesting places to check out:
Authors: Basu, A., Hayden, M., Morrisett, G., and von Eicken, T., Title: A Language-Based Approach to Protocol Construction, Publication: Proc. ACM SIGPLAN Workshop on Domain Specific Languages (WDSL), Place: Paris, France, Jan. 1997. Contents: Describes an extension of Promela, called Promela++, that was used to give a more detailed specification of a protocol stack. From the specification either a standard Promela verification model can be generated, or an efficient implementation of the same protocol. Performance measurements indicate that this can be done without performance penalty.
Authors: Tullmann, P., Turner, J., McCorquodale, J., Lepreau, J.,
Chitturi, A., and Back, G.
Title: Formal Methods: A Practical Tool for OS Implementors
Publication:
HotOS-VI, 6th Workshop on hot topics in operating systems,
See: http://www.eecs.harvard.edu/hotos/
Place: Cape Cod, Mass., 5-6 May 1997, IEEE.
From the abstract:
We applied formal methods to verify properties of the
implementation of the Fluke microkernel's IPC subsystem,
constituting approximately one third of the kernel.
In particular, we have verified the lack of deadlock and
certain liveness properties, with results that apply to
both SMP and uniprocessor environments. The tool we used,
the SPIN model checker, provided an exhaustive concurrency
analysis of the IPC subsystem, unattainable through
traditional OS testing methods.
The tool was immediately accessible to programmers
inexperienced with formal methods. We present our results
as a starting point for a more comprehensive inclusion of
formal methods in practical OS development.
Gerard J. Holzmann (gerard@research.bell-labs.com)