Erigone is a partial reimplementation of the Spin Model Checker. The goal is to facilitate learning concurrency and model checking. Erigone implements a large subset of Promela; no language constructs are added so that programs for Erigone can be used with Spin when more expressiveness and better performance are desired. Erigone can automatically generate diagrams of the state space of simple Promela programs.

EUI is a GUI development environment for Erigone.

VMC is a postprocessor that can generate graphs showing the step-by-step construction and search of the state space during model checking. Click here to watch a video with a demonstration of VMC.

The design of Erigone

• Erigone is single, self-contained, executable file so that installation and use are trivial.
• Erigone produces a detailed trace of the model checking algorithms. The contents of the trace are customizable and a uniform keyword-based format is used that can be directly read or used by other tools.
• Extensive modularization is used in the design of the Erigone program to facilitate understanding the source code. This will also enable researchers to easily modify and extend the program.

Examples

• A random simulation run, which results in a violation of the assertion of mutual exclusion.
• The above random simulation reformatted by the included postprocessor Trace.
• Verification of safety.

Downloads

• The source and binary archives from the Erigone project at Google code: http://code.google.com/p/erigone/.
  The Subversion source code repository can also be accessed there.
• An overview of Erigone: Teaching Concurrency and Model Checking (from the SPIN 2009 Workshop).
  (It can also be downloaded from the Spin webiste.)
• Erigone User's Guide and Quick Start Guide.
• EUI User's Guide and Quick Start Guide.
• The source code of the programs from my textbook Principles of the Spin Model Checker adapted for use with Erigone. For more information on this book click here.
• The source code of the programs from my textbook Principles of Concurrent and Distributed Programming adapted for use with Erigone. For more information on this book click here.

Other relevant software tools

Click here for links to other software tools for teaching concurrency: VN, jSpin, DAJ, iDot.

Implementation

Erigone is written in Ada 2005 for reliability, maintainability and portability. No non-standard constructs are used. The GNAT compiler was used; it is available in free, academic and commercial versions. The Erigone software is copyrighted under the GNU General Public License. Prior to Version 2.0.0, Erigone used a Promela compiler developed by Trishank Karthik Kuppusamy at New York University under the supervision of Edmond Schonberg. This version is available in the SVN repository in the branch ErigoneP.

References

• M. Ben-Ari. Ada for Software Engineers, Springer, 2009
• M. Ben-Ari. Principles of the Spin Model Checker, Springer, 2008..
• M. Ben-Ari. Principles of Concurrent and Distributed Programming, Addison-Wesley, 2005.
• G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual, Addison-Wesley, 2004.

Last update on 9 November 2011.