Distributed MAP in the SpinJa Model Checker

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. Whil...

Full description

Saved in:
Bibliographic Details
Published in:Electronic proceedings in theoretical computer science 2011-10, Vol.72 (Proc. PDMC 2011), p.84-90
Main Authors: Vijzelaar, Stefan, Verstoep, Kees, Fokkink, Wan, Bal, Henri
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2075-2180
2075-2180
DOI:10.4204/EPTCS.72.9