Erigone Model Checker

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:

References

Downloads

Download from GitHub: https://github.com/motib/erigone