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:
[email protected]The 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:
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, [email protected]
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 ([email protected])