基于 ProB 和 LTSmin 的 B 方法符号可达性分析
软件工程
2016-03-15 v1
摘要
我们提出了一种针对 B 方法的符号可达性分析方法，相比传统的显式状态模型检测可带来显著加速。该符号分析通过将 ProB 链接到高性能、语言无关的模型检测器 LTSmin 来实现。该链接通过 LTSmin 的 PINS 接口完成，使得 ProB 能够受益于 LTSmin 的分析算法，同时仅需编写数百行胶水代码，以及使用 ZeroMQ 在 ProB 与 C 之间建立桥梁。ProB 支持多种形式化规范语言（如 B、Event-B、Z 和 TLA）的模型检测。我们的实验基于多种 B 方法和 Event-B 模型，以证明新链接的效率。测试类别包括状态空间生成与死锁检测；但动作检测和不变式检查原则上也可行。在许多情况下我们观察到数个数量级的加速。我们还将结果与其他改进模型检测的方法（如偏序约简或对称约简）进行比较。因此，我们为 B 方法和 Event-B 提供了一种新的可扩展符号分析算法，以及一个未来通过 LTSmin 集成其他模型检测改进的平台。
引用
@article{arxiv.1603.04401,
title = {Symbolic Reachability Analysis of B through ProB and LTSmin},
author = {Jens Bendisposto and Philipp Koerner and Michael Leuschel and Jeroen Meijer and Jaco van de Pol and Helen Treharne and Jorden Whitefield},
journal= {arXiv preprint arXiv:1603.04401},
year = {2016}
}