News
New Book: The Spin Model Checker
Gerald J. Holtzmann has written a new book about the
The Spin Model Checker.
From the Back Cover:
-
Master SPIN, the breakthrough tool for improving software reliability
-
SPIN is the world's most popular, and arguably one of the world's most powerful,
tools for detecting software defects in concurrent system designs.
Literally thousands of people have used SPIN since it was first introduced
almost fifteen years ago. The tool has been applied to everything from the
verification of complex call processing software that is used in telephone
exchanges, to the validation of intricate control software for interplanetary spacecraft.
-
This is the most comprehensive reference guide to SPIN,
written by the principal designer of the tool.
It covers the tool's specification language and theoretical foundation,
and gives detailed advice on methods for tackling the most complex software
verification problems.
All versions of the Bayfront CAPE Tools™ since 1992 have been able to generate SPIN input
from the Bayfront Protocol Dsecription Language (PDL) versions of protocols we used to generate
executable source code.
Existing CAPE v1.5 Generates Spin Formal Theory Validator Input
All versions 1.5 of the CAPE tools are capable of producing output for the Spin simulator/analyzer described in the book
Design and Validation of Computer Protocols
by Gerald J. Holtzmann
(Prentice-Hall 1991 ISBN 0-13-539925-4).
The C source code listing of the
Spin simulator
is given in the appendices of the book and on the web.
A special CAPE option file (SPIN.CTO) is required to enable the production of .SPN Spin output files. Follow the procedure
below to enable SPIN output.
- Download zipped SPIN.ZIP here by saving to a file.
- Unzip the SPIN.CTO file.
- Load the SPIN.CTO configuration file in Options|Open.
- Check Option|Compile dialog box for the text "Simulation Output Enabled"
- Further Compile commands will produce a .SPN file
The Spin software is copyright by Lucent Technologies and Bell Laboratories. It is made available for
commercial use under the
Spin Commercial License.
Reports
Abstract: This application note presents the general style
of c code generation used
by The Bayfront CAPE Tools™ (BCT). Complete details of this process are
presented in chapters 4 though 8 of the BCT v1.5 User's Manual.
copyright © 2006 Bayfront Technologies, Inc.
![[News]](tabnews.jpg)
![[Bayfront Technologies]](ttlcnams.jpg)
![[News and Reports]](ttlnews.jpg)
![[index]](back.gif){kind=small}
Back to index page