Erigone is a partial reimplementation of the Spin Model Checker. The goal is to facilitate learning concurrency and model checking. 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. Erigone implements a subset of Promela that is sufficient for demonstrating the basic concepts of model checking for the verification of concurrent programs. No language constructs are added so that programs for Erigone can be used with Spin when more expressiveness and better performance are desired.
Erigone is written in Ada 2005 for reliability, maintainability and portability. 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.
Postprocessors included in Erigone
- Trace displays the output of a simulation in a tabular form that can be customized in terms of the statements and variables that are displayed.
- VMC (Visualization of Model Checking) generates a sequence of graphs of the state space of a simulation or verification in 'dot' format, one for each step of the verification.
EUI development environment
EUI is an adaptation of the jSpin development environment for use with Erigone. For Windows, download and run the installer
eui-N.exe. For other systems, download the zip archive and open in a clean directory. Download the Erigone model checker and copy
erigone.exe to the directory where you installed EUI. Run:
javaw -jar EUI.jar.
Erigone compatibility of Promela models in my textbooks
The archives that are associated with the following textbooks include Promela programs that are adapted for use with Erigone:
- Principles of the Spin Model Checker, Springer, 2008.
- Principles of Concurrent and Distributed Programming, Addison-Wesley, 2006.
- Overview of Erigone: Tool Paper: Teaching Concurrency and Model Checking. Spin Workshop, 2009, Grenoble, France.
Tutorial on model checking: Mordechai (Moti) Ben-Ari. A primer on model checking. ACM Inroads 1, 1 (March 2010), 40-47. http://doi.acm.org/10.1145/1721933.1721950.
In the program in the second column of page 44,
counter==10. Thanks to Leif Anderson for pointing this out.
- Tutorial on search diversity: Mordechai (Moti) Ben-Ari and Fatima Kaloti-Hallak. Demonstrating random and parallel algorithms with Spin. ACM Inroads 3, 3 (September 2012), 36-38. http://doi.acm.org/10.1145/2339055.2339069.
Download from GitHub: https://github.com/motib/erigone