SpinJa模型中的分布式MAP
Distributed MAP in the SpinJa Model Checker
摘要：
Spin in Java（SpinJa）是Promela建模语言的显式状态模型检查器，也被SPIN模型检查器使用。SpinJa的实现被设计为可扩展和可重用的，它遵循分层的方法，其中每个新层都扩展了前一层的功能。虽然SpinJa初步支持共享内存模型检验，但它还不支持分布式内存模型检验。该工具文件提出了一个分布式实现的最大接受前辈（MAP）搜索算法的SpinJa。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
