\input zb-basic
\input zb-ioport
\iteman{io-port 05571130}
\itemau{Ben-Ari, Mordechai (Moti)}
\itemti{Tool presentation: Teaching concurrency and model checking.}
\itemso{P\u as\u areanu, Corina S. (ed.), Model checking software. 16th international SPIN workshop, Grenoble, France, June 26--28, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02651-5/pbk). Lecture Notes in Computer Science 5578, 6-11 (2009).}
\itemab
Summary: This paper describes software tools for teaching concurrency and model checking. jSpin is an 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.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-02652-2\_5}
\end