Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
复制标题
DOI：
10.1007/s10817-017-9418-4
复制
发表时间：
2018-01-01
期刊：
影响因子：
--
通讯作者：
Lammich, Peter
中科院分区：
文献类型：
--
作者：
Brunner, Julian;Lammich, Peter
我们提出了一个正式的验证和可执行的飞行LTL模型检查，使用充足的集合偏序约简。验证是使用证明助手Isabelle/HOL完成的，涵盖了从抽象正确性证明到生成的SML代码的所有内容。在Doron Peled的论文“Combining Partial Order Reductions with On-the-Fly Model-Checking”的基础上，我们形式化地证明了样本集偏序约简的抽象正确性。这个定理与实际的约简算法无关。然后，我们验证了一个简单的，但表现力的片段Promela的减少算法。我们使用静态偏序约简，它允许分离的偏序约简和模型检查算法的正确性证明和实现。因此，我们在以前的工作中验证的Cava模型检查器可以用作后端，只需进行最小的更改。最后，我们使用逐步细化的方法生成可执行的SML代码。我们测试我们的模型检测器上的一些例子，观察的有效性的偏序约简算法。
We present a formally verified and executable on-the-fly LTL model checker that uses ample set partial order reduction. The verification is done using the proof assistant Isabelle/HOL and covers everything from the abstract correctness proof down to the generated SML code. Building on Doron Peled's paper "Combining Partial Order Reductions with On-the-Fly Model-Checking", we formally prove abstract correctness of ample set partial order reduction. This theorem is independent of the actual reduction algorithm. We then verify a reduction algorithm for a simple but expressive fragment of Promela. We use static partial order reduction, which allows separating the partial order reduction and the model checking algorithms regarding both the correctness proof and the implementation. Thus, the Cava model checker that we verified in previous work can be used as a back end with only minimal changes. Finally, we generate executable SML code using a stepwise refinement approach. We test our model checker on some examples, observing the effectiveness of the partial order reduction algorithm.