The first SPIN workshop, held on 16 October 1995 in Montreal, created a first opportunity for SPIN users to meet and interact informally, to exchange experiences, ideas, theories, wishes, gripes. The proceedings of the first workshop are accessible online via:
http://netlib.bell-labs.com/netlib/spin/ws95/spin95_abstracts.htmlThis year many conferences related to formal methods and verification are organized in New Jersey, as part of the DIMACS Special Year. This includes the conferences such as CAV, LICS, and a series of workshops in our area (see also Appendix 3 below). We will therefore organize the 2nd SPIN Workshop also in New Jersey.
The workshop will be held this year at Bell Labs in Murray Hill, in New Jersey, on Monday August 5, just after LICS96 (Jul 27 - Jul30) and CAV96 (Jul 31-Aug 3) both held in New Brunswick, which is not far from Murray Hill. Details on transportation between Rutgers and Murray Hill will follow when the date of the workshop comes closer.
We will organize some demo sessions for extensions, restrictions, and variations of SPIN (or of any comparable tool that is suggested). We plan to include the real-time extension of SPIN, which was announced at last years workshop, and also one of the commercial extensions.
Also this year we will have a keynote speaker. We are delighted that Moshe Vardi, one of the main contributors to the theory on which SPIN is founded, has accepted our invitation to be the workshops first invited speaker.
Title: SPIN96 -- Second International SPIN Workshop --
Date: Monday August 5 1996 (just after LICS96 and CAV96)
Place: AT&T Bell Laboratories, Murray Hill, NJ
Duration: One day (tentatively: 9am - 5pm)
Keynote speaker: Moshe Vardi, Rice University
Papers: Papers can be up to 20 pages in length and can be
either a report on work in progress or a regular
research paper on work that is somehow related to
the SPIN system .
Demos: Tool demonstrations, of extensions, restrictions
variations, or alternatives, to SPIN, are invited.
Please tell us as early as possible if you plan
to demonstrate software - so that we can make sure
we can set it up properly and make it work.
Dates: The deadline for all contributions is:
Saturday June 15, 1996.
Papers can be submitted electronically, in PostScript
form to any one of the organizers. We will make available
a Proceedings of the workshop in both printed and also, for
the authors that permit us to do so, in electronic form.
Organizers:
Jean-Charles Gre'goire - gregoire@inrs-telecom.uquebec.ca
Gerard Holzmann - gerard@research.bell-labs.com
Doron Peled - doron@research.bell-labs.com
This has been a relatively quiet period in which SPIN has been given some time to stabilize after the two large incremental changes from last year (the addition of the partial order reduction algorithms in version 2.0, and the addition of the LTL translation algorithms in 2.7).
The current version of SPIN is 2.7.7. The more interesting extensions, restrictions and bug fixes can be summarized as follows.
[Abstract: In this paper we present and discuss a number of techniques that can be used in the modeling and veri- fication of electro-mechanical relay circuits. These techniques are based on state machine descriptions of circuits and their functions, and apply validation tools for such descriptions.]
The PostScript version is available online at:
http://www.phil.ruu.nl:80/home/pve/txt/relay.ps
The following is submitted by Gregory Duval (duval@di.epfl.ch) from the Computer Networking Laboratory at EPFL in Lausanne, Sw.
Abstract: This paper reports the results of specifying and verifying the Steam Boiler problem with Promela/SPIN. The problem is to control the level of water in a steam boiler by using different kinds of devices. The water level has to be maintained between two limits (N1 and N2) and can not pass over two limits (M1 and M2) for more than five seconds. The system has to work correctly because the quantity of water present has to be neither too low nor too high; otherwise the steam-boiler can be seriously damaged. Each model represents an abstract level for capturing the original problem requirements. The last model is very detailed and give a first answer to the steam boiler problem. The model is able to drive the system and takes devices failures (pumps, pump controllers, steam and water) into account.
Liveness and safety properties have been checked on the models to insure that the system behavior is correct. An implementation of the system was made in Synchronous C++, a concurrent extension of C++, and linked with a TCL/TK simulation. A presentation of future evolutions of the system is described too. This application shows that SPIN is quite appropriate for developing control process problems from specifications. Some more details about this case study (specifications, reports, models, demos and code) may be found on http://diwww.epfl.ch/w3lti/
What: DIMACS Workshop on Partial Order Methods in Verification
When: July 24-26, 1996
Where: Princeton University, NJ, USA
Speakers: R. Alur, E. Best, I. Castellani, V. Diekert
A. Emerson, P. Godefroid, S. Katz, D. Luckham
A. Mazurkiewicz, M. Nielsen, A. Rabinowitz, W. Penczek,
W. Reisig, G. Rozenberg, M.W. Shields, P.S. Thiagarajan,
W. Thomas, A. Valmari, P. Wolper, G. Wynskel, R. van Glabeek
Organizers: Doron Peled, Vaughan Pratt, Gerard Holzmann
More info at: http://dimacs.rutgers.edu/SpecialYears/1995_1996/schedule.html
End of Appendices.
Gerard J. Holzmann (gerard@research.bell-labs.com)