Closing of Google Code

You can download zip files with source and binary code and learning materials from my web site: software tools and files associated with textbooks.

If you wish to initiate a collaborative development, the projects are also available as repositories on GitHub.

The 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.

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.

Two postprocessors of the trace output are included:

• 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. A video demonstration of VMC can be found at http://screencast.com/t/HNQ5l1lijXsJ.

The EUI development environment

EUI 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 (see the link on this page).

Promela models from my textbooks

The list of downloads includes the following archives that contain versions of Promela models from my textbooks adapted for Erigone:

• psmc-erigone-N.zip for Principles of the Spin Model Checker, Springer, 2008.
• pcpd-erigone-N.zip for Principles of Concurrent and Distributed Programming, Addison-Wesley, 2006.

Implementation

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

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. This has not been updated for a long time; if you can help, I'd appreciate it.

References

• Overview of Erigone: 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.
• 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.

Other relevant software

DAJ 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 left.