Distributed MAP in the SpinJa Model Checker
Software Engineering
2011-11-03 v1 Distributed, Parallel, and Cluster Computing
Abstract
Spin in Java (SpinJa) is an explicit state model checker for the Promela modelling language also used by the SPIN model checker. Designed to be extensible and reusable, the implementation of SpinJa follows a layered approach in which each new layer extends the functionality of the previous one. While SpinJa has preliminary support for shared-memory model checking, it did not yet support distributed-memory model checking. This tool paper presents a distributed implementation of a maximal accepting predecessors (MAP) search algorithm on top of SpinJa.
Cite
@article{arxiv.1111.0374,
title = {Distributed MAP in the SpinJa Model Checker},
author = {Stefan Vijzelaar and Kees Verstoep and Wan Fokkink and Henri Bal},
journal= {arXiv preprint arXiv:1111.0374},
year = {2011}
}
Comments
In Proceedings PDMC 2011, arXiv:1111.0064