B通过ProB和LTSmin的符号可达性分析
Symbolic Reachability Analysis of B through ProB and LTSmin
摘要：
我们提出了一个符号的可达性分析方法B，可以提供一个显着的加速比传统的显式状态模型检验。符号分析是通过链接ProB LTSmin，一个高性能的语言无关的模型检查器。该链接通过LTSmin的PINS接口实现，允许ProB受益于LTSmin的分析算法，同时只需编写几百行胶水代码，以及使用ZeroMQ在ProB和C之间建立桥梁。ProB支持多种形式规约语言的模型检验，如B、Event-B、Z和TLA。我们的实验是基于各种各样的B-Method和Event-B模型，以证明新的链接的效率。测试的类别中有状态空间生成和死锁检测，但动作检测和不变式检查原则上也是可行的。在许多情况下，我们观察到几个数量级的加速。我们还比较了结果与其他方法的改进模型检验，如偏序约简或对称约简。因此，我们提供了一个新的可扩展的，符号分析算法的B-方法和事件B，以及一个平台，通过LTSmin在未来集成其他模型检验的改进。
英文摘要：
We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin's PINS interface, allowing ProB to benefit from LTSmin's analysis algorithms, while only writing a few hundred lines of glue-code, along with a bridge between ProB and C using ZeroMQ. ProB supports model checking of several formal specification languages such as B, Event-B, Z and TLA. Our experiments are based on a wide variety of B-Method and Event-B models to demonstrate the efficiency of the new link. Among the tested categories are state space generation and deadlock detection; but action detection and invariant checking are also feasible in principle. In many cases we observe speedups of several orders of magnitude. We also compare the results with other approaches for improving model checking, such as partial order reduction or symmetry reduction. We thus provide a new scalable, symbolic analysis algorithm for the B-Method and Event-B, along with a platform to integrate other model checking improvements via LTSmin in the future.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
