The proceedings of the 1996 Spin Workshop are now being printed by the AMS and will soon be available. Once available the volume will be included in the list of AMS publications that can be browsed at:
http://www.ams.org/bookstore/(follow the links for 'Books' and 'What's New')
The full title for the volume is:
The Spin Verification System - Second Workshop on the Spin Verification System - Proceedings of a DIMACS Workshopbut among friends the bibliographic reference may be given as:
Proc. Second Workshop on the Spin Verification System held August 5, 1996, Rutgers University, New Brunswick, NJ. Ed. J-C. Gregoire, G.J. Holzmann, and D.A. Peled. Publ. American Mathematical Society, DIMACS/39.(In the listing at the AMS URL you can already find the proceedings for the POMIV workshop on Partial Order Methods, numbered DIMACS/29)
15 Februari 1997The workshop is held as a satellite of TACAS97 at Twente University, The Netherlands, on 5 April this year.
We are looking forward to many participants, good demos, and inspiring talks. Send a note to one of the organizers, e.g., Rom Langerak (langerak@cs.utwente.nl) if you would like to organize a demo, intend to submit a paper, or have proposals for tutorials, panel discussions or anything else that comes to mind to make this workshop of value to you.
Attending the SPIN workshop is free (including lunch). A shuttle-bus will run on April 5 between hotel an workshop. More info, with registration and hotel information:
http://wwwtios.cs.utwente.nl/~tacas97/ http://netlib.bell-labs.com/netlib/spin/ws97/call.html
http://www.enst.fr/~demaille/a2ps.htmla2ps recognizes a file by its extension. A Promela file is recognized by the extension ".pml" -- or one can use the explicit a2ps option "-kpromela"
A little course (in French) for Spin and Promela can also be found at
http://www.enst.fr/~cottin/spin
q?msg,datawill only be executable if the first field in the incoming message also contains the value 'msg.'
A predefined function 'eval()' is part of Spin versions 2.9.3 and later. The eval() function is used to evaluate a variable to yield a value that can be used inside receive arguments as if it were a constant. This makes it possible to make a conditional receive that matches a possibly changing value of a variable. For instance
q?eval(_pid),par2,par3will only be executable for incoming messages with a first field that quals the value of _pid. Note that using
q?_pid,par2,par3instead would specify that the value of (predefined) variable _pid is to be overwritten by the value of the first field in the message, whatever that happens to be.
Abstract: This paper reports the results of specifying, designing, verifying and implementing safe object oriented process control applications. This work gives a solution which enables the synthesis of a general method for addressing problems associated with these procedures. This method has been applied on several case studies by using the SPIN verification tool. An implementation of the lift controller and a graphical simulation have then been realised using Synchronous C++ , a concurrent extension of C++ designed by our team and which is being integrated into Gnu gcc. Liveness and safety properties have been checked on the model to ensure that the system behaviour is correct. This application shows the efficiency of using formal methods in building safe process control applications. It also shows that Synchronous C++ is appropriate for developing process control problems and is easily translatable from synchronous models such as Promela.
Abstract This paper reports the results of specifying and verifying the Steam Boiler problem with Promela/SPIN. Several models of the system have been produced with different degrees of completeness. Each model represents an abstract level for capturing the original problem requirements. The last model is very detailed and gives a first solution to the steam boiler problem. The model is able to drive the system and takes device failures (pumps, pump controllers, steam and water) into account. Liveness and safety properties have been successfully checked on the models to insure that the system behaviour is correct. An implementation of the system has been made using Synchronous C++, a concurrent extension of C++, and linked with the TCL/TK simulation. A presentation of future evolutions of the system is also described. This application shows that SPIN is appropriate for developing control process problems from specifications.
Gerard J. Holzmann (gerard@research.bell-labs.com)