SPIN NEWSLETTER Nr. 20

Contents NewsLetter 20 - October 26, 1997:

Book contents online

We have gained the permission from Prentice Hall to make an digital version available of the contents of the 1991 book that documents much of the original design of Spin. The contents is available in either Acrobat PDF format, or in standard Postscript. The URL's are: http://cm.bell-labs.com/cm/cs/what/spin/Doc/Book91_pdf.tar.gz (about 1.4 MB) and http://cm.bell-labs.com/cm/cs/what/spin/Doc/Book91_ps.tar.gz (about 830 KB).

The Current Spin Version

The current version of Spin is Version 3.0.4. There are no great changes from 3.0, just a few relatively minor bug fixes. If, however, you were unfortunate enough to pick up an Xspin version numbered xspin303.tcl, you'd do well to retrieve a new copy. That version of Xspin has a trivial flaw that unnecessarily complicates the verification process.
If you have 'dot' installed (a graph layout tool from Steven North and colleagues), the new version of Spin gives an option to generate a structural view of a Promela system (i.e., showing how processes communicate via channels). You'll need a small awk-script to turn the output from spin 3.0.4 into a postscript file. Send mail if you'd like to experiment with this option.

User Queries

1. Procedures in Promela
Dennis Dams, Rob Gerth, and Martin Steffen, from the Technical University in Eindhoven, the Netherlands, have studied the possibilities for including a procedure, or function, concept in Promela, in the context of their work on the Vires project ( see http://www.win.tue.nl/cs/fm/vires/). They write: The note is accessible at: http://www.win.tue.nl/cs/fm/Dennis.Dams/procs/procs.html One problem, also discussed in the note, is how to give clean semantics to notations such as: 
	if :: x == call p() :: x != call p() fi
Note that the (function) calls cannot be evaluated without side-effects in this case. If you have ideas on problems like these, please read the full note and send feedback to the authors.

2. Emacs question 

	From stc.com!nathan Mon Sep 15 18:31:04 EDT 1997
	From: Nathan Inada 
	Organization: Software Technologies Corporation
	Subject: emacs promela mode ?
	
	Hi,
	Does anyone have a Promela mode for emacs, and/or know
	if cc-mode can be tweeked to give such?
	
	Thanks in advance
	nathan

3. Java question 

	From adm.csc.ncsu.edu!kct Thu Oct 16 10:59:12 EDT 1997
	From: K C Tai 
	Subject: SPIN-like tool for Java
	
	I am using Java to teach concurrent programming this semester.
	I would like to know whether someone has developed or is
	developing a SPIN-like tool for Java. If you have such 
	information, please let me know.
	
	I think a SPIN-like tool for Java has a great commercial
	potential.
	
	KC Tai

Interesting URLs

1. A Verification Course
Karen Bernstein is developing a cours on verification/validation for Masters students. Much of the material is on the web and interesting to browse. With Karen's permission (cs.depaul.edu!kbernstein), here is the url: http://dpelab.cs.depaul.edu/se533/
(Send us a message if you know of similar websites.)

2. A Project description
An interesting description of a succesful application of Spin to an industrial development project: http://hzswww.nl.lucent.com/~wboeke/papers/ssm_prtcl_valid.html

Recent Papers

End of Newsletter Nr. 20.

Spin (spin_list@research.bell-labs.com)