Distributed MAP in the SpinJa model checker

S.J.J. Vijzelaar; K. Verstoep; W.J. Fokkink; H.E. Bal

doi:10.4204/EPTCS.72

Distributed MAP in the SpinJa model checker

S.J.J. Vijzelaar, K. Verstoep, W.J. Fokkink, H.E. Bal

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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.

Original language	English
Title of host publication	Proceedings of 10th Workshop on Parallel and Distributed Methods in Verification (PDMC'11). 14 July 2011, Snowbird, Utah
Editors	J. Barnat, K. Heljanko
Pages	84-90
DOIs	https://doi.org/10.4204/EPTCS.72
Publication status	Published - 2011

Access to Document

10.4204/EPTCS.72

Cite this

@inproceedings{fcb5b6aac2ac4843845a21525631f4d5,

title = "Distributed MAP in the SpinJa model checker",

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.",

author = "S.J.J. Vijzelaar and K. Verstoep and W.J. Fokkink and H.E. Bal",

year = "2011",

doi = "10.4204/EPTCS.72",

language = "English",

pages = "84--90",

editor = "J. Barnat and K. Heljanko",

booktitle = "Proceedings of 10th Workshop on Parallel and Distributed Methods in Verification (PDMC'11). 14 July 2011, Snowbird, Utah",

}

Distributed MAP in the SpinJa model checker. / Vijzelaar, S.J.J.; Verstoep, K.; Fokkink, W.J. et al.
Proceedings of 10th Workshop on Parallel and Distributed Methods in Verification (PDMC'11). 14 July 2011, Snowbird, Utah. ed. / J. Barnat; K. Heljanko. 2011. p. 84-90.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Distributed MAP in the SpinJa model checker

AU - Vijzelaar, S.J.J.

AU - Verstoep, K.

AU - Fokkink, W.J.

AU - Bal, H.E.

PY - 2011

Y1 - 2011

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

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

U2 - 10.4204/EPTCS.72

DO - 10.4204/EPTCS.72

M3 - Conference contribution

SP - 84

EP - 90

BT - Proceedings of 10th Workshop on Parallel and Distributed Methods in Verification (PDMC'11). 14 July 2011, Snowbird, Utah

A2 - Barnat, J.

A2 - Heljanko, K.

ER -

Distributed MAP in the SpinJa model checker

Abstract

Access to Document

Fingerprint

Cite this