Producing Short Counterexamples Using "Crucial Events"
Producing Short Counterexamples Using "Crucial Events"
复制标题
使用“关键事件”制作简短的反例
DOI：
10.1007/978-3-540-70545-1_47
复制
发表时间：
2008
影响因子：
0.8
通讯作者：
V. Garg
中科院分区：
文献类型：
--
作者：
Sujatha Kashyap;V. Garg
理想情况下，模型检查工具应该成功地处理状态空间爆炸，以完成系统验证，同时在存在错误时提供简短的反例。偏序约简[1,2]等技术在处理状态空间爆炸方面非常有效，但不能产生简短的反例。另一方面，定向模型检查[3,4]技术可以找到简短的反例，但在没有错误的情况下容易出现状态空间爆炸。据我们所知，目前还没有一种技术能同时满足这两个要求。本文提出了这样一种技术。
Ideally, a model checking tool should successfully tackle state space explosion for complete system validation, while providing short counterexamples when an error exists. Techniques such as partial order (p.o.) reduction [1,2] are very effective at tackling state space explosion, but do not produce short counterexamples. On the other hand, directed model checking [3,4] techniques find short counterexamples, but are prone to state space explosion in the absence of errors. To the best of our knowledge, there is currently no single technique that meets both requirements. We present such a technique in this paper.
For a subset of CTL, which we call CETL (Crucial Event Temporal Logic), we show that there exists a unique minimum set of events in each program trace whose execution is both necessary and sufficient to lead to an error state. These events are called "crucial events". We show how crucial events can be used to produce short counterexamples, while also providing state space reduction.
We have implemented the techniques presented here as an extension to the model checker SPIN, called SPICED (Simple PROMELA Interpreter with Crucial Event Detection). Experimental results are presented.