Usage: spin -c specIt can be considerably more informative than the standard tracebacks. Inspiration for this new feature (and for event traces) was a brief comparison of Spin with one of its early predecessors trace from 14 years ago. In this case, trace turned out to have some options that had been lost in the succession of tools.
Usage: spin -M spec or: spin -t -M specwhich produces the file spec.ps The second form above converts an error trail into Postscript.
Usage: spin -f "p" or : spin -F file with: p as the first line in 'file'
The papers are the updated versions of the preprint papers that are still online as the workshop proceedings. The table of contents for the volume is:
Author: Michael J. Ferguson, INRS-Telecom.UQuebec.CA!mike Title: Formalization and Validation of the Radio Link Protocol (RLP1), Publication: Computer Networks, V29 N3, pp. 357-372. Contents: Discusses the validation of a radio link protocol (RLP1) with Spin, as part of the protocol's standardization. It is argued that a suite of accepted formal notations is necessary to formalize the many different parts of a protocol standard.
Author: Gerard Holzmann, [email protected] Title: The model checker Spin Publication: IEEE Trans. on Software Engineering, May 1997, V23 N5, pp. 279-295. Contents: The paper gives an overview of the design and structure of the verifier, reviews its theoretical foundation, and gives an overview of significant practical applications to date. Title: Designing Bug-Free Protocols with Spin Publication: Computer Communications Journal, March 1997, V20 N2, pp. 97-105. Contents: Outlines the use of Spin to address protocol design problems. As an example it considers the verification of a published protocol for implementing synchronous rendezvous operations in a distributed system.