A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties
A Parallel Stratified Model Checking Technique/Tool for Leads-to Properties
复制标题
一种并行分层模型检查技术/工具，用于引导属性
DOI：
10.1109/isssr53171.2021.00011
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Ogata Kazuhiro
中科院分区：
文献类型：
--
作者：
Do Canh Minh;Phyo Yati;Riesco Adrian;Ogata Kazuhiro
L + 1-DCA 2L 2 MC是一种新的模型检测方法，它可以有效地缓解模型检测中状态空间爆炸的问题。正如其名称所示，L + 1-DCA 2L 2 MC专用于引线特性。本文描述了L+1-DCA 2L 2 MC的并行版本及其支持工具，在Chandy和Misra设计的UNITY时序逻辑中，引出时态连接词起着重要的作用，并在UNITY中进行了大量的实例研究，证明了许多系统需求可以用引出属性来表示。因此，它是值得致力于财产。实验结果表明，该工具能够提高模型检测的运行性能。
The L+1-layer divide & conquer approach to leads-to model checking (L + 1-DCA2L2MC) is a new technique to mitigate the state space explosion in model checking. As shown by the name, L + 1-DCA2L2MC is dedicated to leads-to properties. The paper describes a parallel version of L+1-DCA2L2MC and a tool that supports it. In a temporal logic called UNITY designed by Chandy and Misra, the leads-to temporal connective plays an important role and many case studies have been conducted in UNITY, demonstrating that many systems requirements can be expressed as leads-to properties. Hence, it is worth dedicating to the properties. The paper also reports on some experiments that demonstrate that the tool can increase the running performance of model checking.