Distributed MAP in the SpinJa Model Checker

TL;DR

This paper introduces a distributed implementation of the MAP search algorithm within SpinJa, enhancing its capabilities for distributed-memory model checking of Promela models.

Contribution

It presents the first distributed-memory MAP algorithm integrated into SpinJa, extending its support from shared-memory to distributed environments.

Findings

Enables scalable distributed model checking in SpinJa.

Demonstrates effective MAP search in distributed settings.

Improves the extensibility of SpinJa for distributed algorithms.

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.