Tool Presentation: Teaching Concurrency and Model Checking

This paper describes a set of software tools developed for teaching concurrency and model checking. jSpin is an elementary development environment for Spin that formats and filters the output of a simulation according to the user’s specification. SpinSpider uses debugging output from Spin to generate a diagram of the state space of a Promela model; the diagram can be incrementally displayed using iDot. VN supports teaching nondeterministic finite automata. The Erigone model checker is a partial reimplementation of Spin designed to be easy to use, well structured and well documented. It produces a full trace of the execution of the model checker in a format that is both readable and amenable to postprocessing.

• Type: Conference
• Year: 2009
• Where: SPIN
• Authors: Mordechai Ben-Ari
• Keywords: Erigone Model Checker, Model Checker, Spin, SPIN 2009, Theoretical Computer Science