http://netlib.bell-labs.com/netlib/spin/ws98/call.htmlWe are delighted to announce that the keynote speaker at the SPIN98 workshop will be:
Prof. Amir Pnueli, Weizmann Institute of Science, IsraelThis 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.
* June 20, 1998 -- demo and tutorial proposals * Aug. 20, 1998 -- deadline for papers
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).
http://rodin.stanford.edu/ptl/index.html http://www.es.ele.tue.nl/geert/research/research_ptl.html
Title: Formal analysis of a space craft controller using Spin. Authors: Klaus Havelund, Mike Lowry, John Penix Email: havelund@ptolemy.arc.nasa.gov Pub: NASA/Ames Tech. Report #1770, April 1998 Contents: This report documents an application of the finite state model checker Spin to formally verify a multi-threaded plan execution programming language. The plan execution language is one component of NASA's New Millenium Remote Agent, an artificial intelligence based spacecraft control system architecture that is scheduled to launch in December 1998 as part of the Deep Space 1 mission to Mars. [..] A total of 5 errors were identified, 4 of which were important. This is regarded as a very successful result. According to the Remote Agent programming team the effort has had a major impact, locating errors that would probably not have been located otherwise and identifying a major design flaw not yet resolved at the time of writing.
Title: Validating Requirements for Fault Tolerant Systems using Model Checking Authors: F. Schneider, S.M. Easterbrook, J.R. Callahan, G.J. Holzmann Email: Francis.L.Schneider@jpl.nasa.gov Pub: Proc. ICRE98, Int. Conf. on Requirements Engineering, April 1998 Abstract: Model checking is shown to be an effective tool in validating the behavior of a fault tolerant embedded spacecraft controller. The case study presented here shows that by judiciously abstracting away extraneous complexity, the state space of the model could be exhaustively searched allowing critical functional requirements to be validated down to the design level. Abstracting away detail not germane to the problem of interest leaves by definition a partial specification. The success of this procedure shows that it is feasible to effectively validate a partial specification with this technique. Three anomalies were found in the system. One was an error in the detailed requirements, and the other two were missing/ambiguous requirements. Because the method allows validation of partial specifications, it is also an effective approach for maintaining fidelity between a co-evolving specification and an implementation.
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, ...).
spec-patterns@cis.ksu.eduThe 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
Spin (spin_list@research.bell-labs.com)