SPIN NEWS - Nr. 11 - April 16, 1996

Contents of this NewsLetter:

• SPIN96 Workshop Update
  • Financial support for students
  • Travel arrangements, etc.
• SPIN Version 2.8.1
  • An important upgrade.
• Some Recent Papers
  • B. Boigelot, and P. Godefroid, Belgium/USA)
  • J.C. Corbett, Hawaii

Financial support for students

A small amount of funds is available to provide financial support for graduate students who would like to attend the workshop, but cannot do so without support. If you'd like to qualify for support for hotel and travel to attend the SPIN96 workshop, please send an application to us as soon as possible, but in any case before Saturday June 15, 1996 at the very latest, attaching a brief supporting statement from your supervisor (email is preferred).

The deadline for paper submissions is June 15 1996. Please note that papers that are included in the DIMACS Proceedings of the workshop must be original contributions, not previously published. Depending on the number of submissions, though, we may consider also other contributions for presentation at the workshop itself, and for inclusion in the (preprint) participants proceedings. Contributions selected for the final DIMACS proceedings will also have to pass a reviewing/editing cycle (following DIMACS rules).

Travel arrangements, etc.

It is probably good to note that the 1996 Olympic Games in Atlanta will end close to the start of our workshop (they end on August 3, our workshop is August 5). The extra flow of travelers may make it hard to make reservations for flights also in out of New York close to this date... Make your travel arrangements early! There are good connections between New York or Newark airport to New Brunswick (the Rutgers campus where our workshop is held this year). DIMACS recommends two hotels: the Holiday Inn or the Comfort Inn. More information: http://dimacs.rutgers.edu (or "telnet info.rutgers.edu 90")

SPIN Version 2.8.1

An important upgrade

The current version of SPIN (on netlib.bell-labs.com in directory /netlib/spin) contains some important changes:

• We discovered that the standard nested depth-first search method is not in all cases compatible with partial order reduction methods. The change that guarantees compatibility is relatively small, and can even improve the time and memory requirements of SPIN verification runs for LTL model checking (i.e., with runtime option -a, for reporting presence or absence of acceptance cycles, with or without a Never Claim, and with or without an LTL formula).
• A similar incompleteness existed in the implementation of the nested depth first search algorithm for non-progress cycles (i.e., runtime option -l). In this case, the required correction can increase the time and memory requirements of a verification run (the difference we measured was an increase of approx. 10% in time and in memory for our standard tests).
• To avoid incurring this potential overhead for other search modes, SPIN 2.8.1 supports a new compile time directive -DSAFETY When defined, the pan.c source is compiled for best performance on safety properties only (with or without partial order reduction and with or without bitstate hashing). If -DSAFETY is not defined, the verifier is compiled for general safety and liveness proofs, by including full support for LTL model checking, and code for runtime options -a and -l.
• Another way, perhaps better way, to avoid the overhead, and to take full advantage of partial order reductions at the same time, is to use an LTL property instead of SPIN's builtin notion of progress labels. Absence of non-progress cycles equates to proving that an LTL formula of the form

  	"<>[]!p"
  

  cannot be satisfied, where "p" is a condition of the form

  	"process_name[pid]@label_name"
  

  (or an arbitrary boolean combination of similar terms).
• The new X-interface of SPIN, Xspin version 2.8.1, has been updated to exploit all the above changes and will automatically setup the compilations for best performance in each case.

  SPIN version 2.8.1 is also fully compatible with PC's. SPIN itself (a pre-compiled executable is included in the file pc_spin281.zip) works with any operating system (Windows 3.1, Windows NT, or Windows95), provided that you have the gcc executables (shareware) also installed. Xspin, SPIN's Tck/Tk interface works only with Windows95 (there is a bug in Tck/Tk itself when used with Windows 3.1 that does not seem likely to be fixed anytime soon by the Tcl/Tk people).

• Model checking in practice: an analysis of the ACCESS.bus protocol using SPIN.
  by Bernard Boigelot (University of Liege) and Patrice Godefroid (Bell Laboratories)
  Proc. Formal Methods Europe'96, Oxford, March 1996. Lecture Notes in Computer Science, Vol. 1051, pp 465-478, Springer-Verlag.
  Contact: Patrice Godefroid, god@bell-labs.com

  From the Abstract: This paper presents a case study of the use of model checking for analyzing an industrial protocol, the ACCESS.bus protocol. Our analysis of this protocol was carried out using SPIN, an automated verification system which includes an implementation of model-checking algorithms. A model of the protocol was developed, and properties expressed by linear-time temporal-logic formulas were checked on this model. This analysis revealed subtle flaws in the design of the protocol. Developers who worked on implementations of ACCESS.bus were unaware of these flaws at a very late stage of their development process. We also present suggestions for solving the detected problems.

• Evaluating deadlock detection methods for concurrent software.
  by J.C. Corbett, University of Hawaii.
  IEEE Transactions on Software Engineering, March, 1996, Vol. 22, No. 3, pp. 161-180.
  Contact: Jay Corbett, corbett@hawaii.edu

  From the Abstract: In this paper, we carry out an evaluation of three techniques for combatting the state explosion problem in deadlock detection: reachability search with a partial order state space reduction [SPIN], symbolic model checking [SMV], and inequality necessary conditions [INCA]. We justify the method used for the comparison, and carefully analyze several sources of potential bias.

End of Newsletter Nr. 11.