SPIN NEWS - Nr. 9 - February 5, 1996

Contents of this NewsLetter:

The Second SPIN Workshop -- SPIN96

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://spinroot.com/spin/Workshops/ws95/spin95_abstracts.html
This 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 - [email protected]
               Gerard Holzmann        - [email protected]
               Doron Peled            - [email protected]

SPIN Updates since last NewsLetter

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.

Extensions

Restrictions

Bug Fixes

Appendix 1 - Some Recent Papers

Appendix 2 - The Steam Boiler Problem

The following is submitted by Gregory Duval ([email protected]) 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/

Appendix 3 - POMIV Workshop Announcement

   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.

End of Newsletter Nr. 9.