The jSpin development environment for Spin

jSpin is a graphical user interface for the Spin model checker that is used for verifying concurrent and distributed programs. The user interface of jSpin is simple and consists of a single window with menus, a toolbar and three adjustable text areas. Spin option strings are automatically supplied and the Spin output is filtered and presented in a tabular form. All aspects of jSpin are configurable: some at compile time, some at initialization through a configuration file and some at runtime.

The EUI development environment for Erigone

EUI is a version of jSpin for the Erigone Model Checker. A binary of Erigone is included in the Windows installer of EUI. If you use the zip archive, obtain and download/build Erigone from its project page. Erigone does not need a C compiler.

Spin Spider - a graphical representation of the state space

Spin Spider is a postprocessor for the Spin debugging output that creates a description of the diagram in the dot graphics language for the entire state space of a Promela program. Spin Spider has been integrated into jSpin, although it can be run from the command line as a standalone tool. Optionally, you may wish to use iDot to incrementally display the dot graphs.

The VMC postprocessor for Erigone generates graphs that show the model checking algorithm incrementally.

Required software

jSpin needs Spin and SpinSpider needs dot from Graphviz; these are included in the Windows installer and in the file jSpin-bin.zip. A C compiler is also needed for running Spin. I suggest MinGW and for Windows a single-file minimal installation can be downloaded. Feel free to replace these software packages with newer versions that you install yourself. Be sure to check if you need to change the configuration file.

Warning The latest version of MinGW mingw-get-inst-20111118.exe causes problems (a missing dll) when invoking the compiler from within jSpin. The workaround is to install only the C compiler. (Thanks to Bernhard Drabant.)

Other projects for teaching concurrency

DAJ -- interactive execution of distributed algorithms.