SpinJa 模型检测器中的分布式 MAP
软件工程
2011-11-03 v1 分布式、并行与集群计算
摘要
Spin in Java (SpinJa) 是一个用于 Promela 建模语言的显式状态模型检测器,该语言也被 SPIN 模型检测器使用。SpinJa 的设计注重可扩展性和可重用性,其实现采用分层方法,每一新层都扩展前一层的 functionality。虽然 SpinJa 已初步支持共享内存模型检测,但尚未支持分布式内存模型检测。本文介绍了一种在 SpinJa 之上实现的分布式最大接受前驱(MAP)搜索算法。
引用
@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}
}
备注
In Proceedings PDMC 2011, arXiv:1111.0064