Optimising the ProB model checker for B using partial order reduction
Optimising the ProB model checker for B using partial order reduction
复制标题
使用偏序约简优化 B 的 ProB 模型检查器
DOI：
10.1007/s00165-015-0351-1
复制
发表时间：
2014
影响因子：
1
通讯作者：
Michael Leuschel
中科院分区：
文献类型：
--
作者：
Ivaylo Dobrikov;Michael Leuschel
部分降阶在对抗低级形式主义的状态爆炸问题上已经非常成功，但到目前为止，对于诸如B、Z或TLA+之类的高级形式主义的模型检查几乎没有任何影响。本文试图在Event-B的上下文中解决这个问题，它具有更细粒度的事件，从而增加了事件独立性和偏序约简的可能性。在这项工作中，我们提供了一个详细的描述，在ProB的显式状态模型检查的部分订单减少的技术进行评估的各种模型。讨论了该方法的实现，该方法基于新的基于约束的分析。此外，我们给出了一个全面的描述，详细说明了实现到LTL模型检查器的ProB检查LTL-X公式。
Partial order reduction has been very successful at combatting the state explosion problem for lower-level formalisms, but has thus far made hardly any impact for model checking higher-level formalisms such as B, Z or TLA+. This paper attempts to remedy this issue in the context of Event-B, with its much more fine-grained events and thus increased potential for event-independence and partial order reduction. In this work, we provide a detailed description of a partial order reduction for explicit state model checking in ProB. The technique is evaluated on a variety of models. The implementation of the method is discussed, which is based on new constraint-based analyses. Further, we give a comprehensive description for elaborating the implementation into the LTL model checker of ProB for checking LTL−Xformulae.
登录
查看更多内容
B 的对称性简化模型检查
DOI：
--
发表时间：
2007
期刊：
Theoretical Aspects of Software Engineering
影响因子：
--
作者：
E. Turner;M. Leuschel;Corinna Spermann;M. Butler
通讯作者：
M. Butler
B 的定向模型检查：评估和新技术
DOI：
--
发表时间：
2010
期刊：
Brazilian Symposium on Formal Methods
影响因子：
--
作者：
M. Leuschel;J. Bendisposto
通讯作者：
J. Bendisposto
通过Event-B模型的逐步调度推导并发程序
影响因子：
1
作者：
Pontus Boström;Fredrik Degerlund;K. Sere;M. Waldén
通讯作者：
M. Waldén
DOI：
--
发表时间：
1989
期刊：
Parallel Architectures and Languages Europe
影响因子：
--
作者：
A. Valmari
通讯作者：
A. Valmari
用于多核 LTL 模型检查的偏序约简
DOI：
--
发表时间：
2014
期刊：
Haifa Verification Conference
影响因子：
--
作者：
A. Laarman;Anton Wijs
通讯作者：
Anton Wijs