[News] [Bayfront Technologies] [News and Reports]


New Book: The Spin Model Checker

Gerald J. Holtzmann has written a new book about the The Spin Model Checker. From the Back Cover: 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.
  1. Download zipped SPIN.ZIP here by saving to a file.
  2. Unzip the SPIN.CTO file.
  3. Load the SPIN.CTO configuration file in Options|Open.
  4. Check Option|Compile dialog box for the text "Simulation Output Enabled"
  5. 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.


AppNote 5: CAPE v1.5 C Coding Style

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.
[index] Back to index page
Valid HTML 4.01 Transitional
copyright © 2006 Bayfront Technologies, Inc.