Tool Presentation: Teaching Concurrency and Model Checking

13 years 6 months ago
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.
Mordechai Ben-Ari
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SPIN
Authors Mordechai Ben-Ari
Comments (0)