SPIN NEWS - Nr. 1 - January 3, 1995

There are close to 1,100 sites where the SPIN verification software is now installed. This is a nice enough number to start supporting SPIN users a little more actively. This first issue of the SPIN News mailing goes only to a select number of people (approx 140) that have in the last few months asked about the verifier and its applications, and a few honorary recipients. The next issue will only go to those who ack this mail (see pt 1. below).

The main reason for these mailings is to have a channel to send out brief reminders whenever an update of the SPIN software takes place - bug fixes, extensions, or major improvements such as the switch to Version 2.0.

Two other types of items can also be included in such mailings: (a) answers to frequently asked questions from SPIN users about modeling, complexity control, algorithms etc., and (b) announcements or question from people who would like to get in touch with other SPIN users.

The new SPIN Version 2.0, available from January 1 1995 on, includes a significantly richer specification language, as well as an implementation of a partial order reduction technique that preserves all safety and liveness properties, and that is compatible with all existing verification modes supported by SPIN. With the reduction, problem sizes of yet another order of magnitude larger may have come within reach of formal verification techniques.

Attached below is a quick summary of the main projects that are being pursued with SPIN, as far as I am aware of them at least. Since several projects are pursued in parallel in different places, it may be useful to distribute this type of information on a more regular basis to the SPIN mailing list.

  1. If you would like to be on the list to receive these mailings, please send a one line message by return mail, saying just: `subscribe to SPIN list'
  2. If you would like to add something to the project list below (or modify an existing entry) - let me know.
  3. If you have a question or announcement that could be of especial value to other SPIN users (e.g. papers you've written, or extensions you've made, or would like other to make) - send the information to me and i'll collect such things for this mailing list.
  4. If you'd like to volunteer to moderate this mailing list, let me know!
  5. Feel free to forward this mail to others whom you think might be interested in this list or the SPIN software.

Appendix:

Some of the projects to apply or extend the SPIN software.

  1. Real-Time Extensions based on the Alur-Dill algorithm
       contact: Costas Courcoubetis, Stavros Tripakis
    	courcou@ics.forth.gr
    	tripaki@ics.forth.gr
    
  2. Other extensions for specifying real-time properties:
       contact: Tadanori Mizuno
    	mizuno@cs.shizuoka.ac.jp
    
  3. Extensions for statistical simulations
       contact: Roberto Manione
    	manione@cselt.stet.it
    
  4. Extensions for hardware generation; hardware/software codesign
       contact: Geoffrey Brown
    	gbrown@ee.cornell.edu
    
  5. Extensions for modeling remote procedure calls and multi-threaded processes in distributed computing environments such as DCE and ANSA.
       contact: Joe Lin
    	fjlin@bellcore.com
    
  6. Extensions and applications of SPIN to feature-interaction problems in telecommunication software.
       contact: Joe Lin
    	fjlin@bellcore.com
    
  7. Extensions for sleep-set based partial order reduction
       contact: Pierre Wolper, Patrice Godefroid
    	pw@montefiore.ulg.ac.be
    	god@research.att.com
    
  8. Extensions of Xspin to allow breakpointing
       contact: Thierry Cattel
    	cattel@ltidec1.epfl.ch
    
  9. Modelling and verification of the Harmony multiprocessor real-time kernel
       contact: Thierry Cattel
    	cattel@ltidec1.epfl.ch
    
  10. Translators from Lotos to Promela
       contact: Nicholaos Petalidis
    	npetalid@cee.hw.ac.uk
       contact: Stephane Baier
    	baier@res.enst.fr
    
  11. A port of Spin version 1.6 to the Macintosh
       contact: Bob Johnston
    	70302.1761@compuserve.com
    
  12. Translator from SDL to Promela
       contact: Graham Wheeler
    	gram@aztec.co.za
    
  13. Extension for reduction using compositional approach and context constraints
       contact: Shing-chi Cheung
    	scc@cs.ust.hk
    
  14. Verification of railway signaling: train data bus, relay circuits, client-server protocols.
       contact: Peter van Eijk
    	pve@cvi.ns.nl
    

Gerard J. Holzmann (gerard@research.bell-labs.com)