erigone

Low Activity

Project Summary

Analyzed 6 days ago based on code collected 6 days ago.

The Erigone model checkerErigone 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.

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.

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.

The EUI development environmentEUI is a development environment for use with Erigone. It is an adaptation of the jSpin environment for Spin and can be accessed from the jspin project page (link on in the right-hand panel of this page). The SpinSpider component of jSpin for generating a diagram of the state space is integrated into Erigone.

ImplementationErigone is written in Ada 2005 for reliability, maintainability and portability.

Before version 2, Erigone used a Promela compiler that was written by Trishank Karthik Kuppusamy, a student at New York University, under the supervision of Edmond Schonberg. This compiler can be accessed from the SVN repository under the branch ErigoneP.

Note for Mac users A workaround is needed when Erigone is compiled for "Snow Leopard". An executable file for this system (contributed by Michael Walker) is available on the Downloads page.

Archives of Promela models for use with ErigoneThe archives psmc-erigone-N.zip and pcpd-erigone-N.zip contain source programs from my books (Principles of the Spin Model Checker, Springer, 2008. ISBN: 978-1-84628-769-5; Principles of Concurrent and Distributed Programming, Addison-Wesley, 2006. ISBN 0-321-31283-X.) that have been adapted for Erigone.

Other relevant softwareDAJ is an interactive execution of distributed algorithms. VN is a tool for visualizing nondeterminism. Links to the projects for these tools are given on the right.