SPIN NEWSLETTER Nr. 22

Contents NewsLetter 22 - April 9, 1998:

SPIN98 Workshop News

The next Spin Workshop is a satellite of the PSTV/FORTE98 Conference in Paris, and will be held on Monday November 2, 1998. The call for contributions can be found at:
	
http://netlib.bell-labs.com/netlib/spin/ws98/call.html
We are delighted to announce that the keynote speaker at the SPIN98 workshop will be:
	Prof. Amir Pnueli, Weizmann Institute of Science, Israel
This year, the best papers from the workshop will also be considered for publication in a special section of the new Springer journal STTT (Software Tools for Technology Transfer). More details on this will follow.
The most important deadlines for the workshop are:
 * June 20, 1998 -- demo and tutorial proposals
 * Aug. 20, 1998 -- deadline for papers

Spin Version 3.2

The current version of Spin/Xspin is 3.2.0. The main new feature of the new version is a limited support for procedures, which should facilitate the specification of models somewhat more succinctly. The extension was inspired by work of Klaus Havelund (see Recent Papers).
An inline procedure definition can appear anywhere a proctype declaration can appear (i.e., globally) and looks as follows:
	inline functionname(x, y) {
		...a promela fragment...
	}
The procedure call can appear anywhere a statement can appear:
	functionname(4, a);
The body of the procedure is inlined by the Spin parser, with proper parameter matching and replacement, but the source line references are properly preserved for simulations. Recursive inlines are also allowed, but of course not cyclic ones. There is a small example of the use of these inline procedures in the Test directory of the distribution file for version 3.2 (Test/abp).

Interesting URLs

The following urls point to propositional temporal validity checkers. Both urls allow you to evaluate PTL formulae online.
http://rodin.stanford.edu/ptl/index.html
http://www.es.ele.tue.nl/geert/research/research_ptl.html

Recent Papers

Appendix:

The following is a request sent in by Matt Dwyer (cis.ksu.edu!dwyer).
REQUEST FOR EXAMPLE REQUIREMENTS FOR FINITE-STATE VERIFICATION
As part of a project to construct a pattern system for the property specifications of finite-state verification tools, we are soliciting examples of requirements that might be verified with those tools (e.g., SPIN, SMV, CWB-NC, ...).
Such requirements typically restrict the occurrence/order of states/events in the finite-state model of the system. Examples include:
  o "After every occurrence of X there must be an occurrence of Y."
  o "Between a P and a Q there can never be an X." 
We are interested in both natural language descriptions of the requirements as well as expressions of requirements in a formal specification language (e.g., LTL, CTL, regular expressions, ...).
Send example requirements or citations/references to such requirements to
   spec-patterns@cis.ksu.edu
The current version of the specification pattern system can be found at
    http://www.cis.ksu.edu/~dwyer/spec-patterns.html
If you have any comments about or contributions that you'd like to make to the specification patterns project we encourage you to send them to the address given above.
Matt Dwyer
George Avrunin
James Corbett

End of Newsletter Nr. 22.

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