Counterexample Explanation by Anomaly Detection
Counterexample Explanation by Anomaly Detection
复制标题
DOI：
10.1007/978-3-642-31759-0_5
复制
发表时间：
2012-07
期刊：
影响因子：
--
通讯作者：
S. Leue;Mitra Tabaei Befrouei
中科院分区：
文献类型：
--
作者：
S. Leue;Mitra Tabaei Befrouei
由于模型检查工具生成的反例只是模型中故障的症状，因此需要大量的手工工作来定位故障，而故障是模型中存在反例的根本原因。在本文中，我们提出了一种自动化的方法来解释并发系统中出现死锁的症状的反例。我们的方法是基于对一组反例的分析，这些反例可以由模型检查工具（如SPIN）生成。通过将反例集与不会死锁的正确跟踪集进行比较，可以提取许多动作序列，帮助模型设计人员定位发生死锁的原因。我们首先认为，提取这些序列的明显方法是通过顺序模式挖掘和对比模式，这是死锁反例轨迹的典型方法，但不是典型的非死锁轨迹，由于问题的固有复杂性而失败。然后，我们建议提取特定长度的子字符串，这些子字符串只出现在反例集合中，以解释死锁的发生。我们使用了一些案例研究来展示我们方法的有效性，并将其与反例解释问题的替代方法进行比较。
Since counterexamples generated by model checking tools are only symptoms of faults in the model, a significant amount of manual work is required in order to locate the fault that is the root cause for the presence of counterexamples in the model. In this paper, we propose an automated method for explaining counterexamples that are symptoms of the occurrence of deadlocks in concurrent systems. Our method is based on an analysis of a set of counterexamples that can be generated by a model checking tool such as SPIN. By comparing the set of counterexamples with the set of correct traces that never deadlock, a number of sequences of actions are extracted that aid the model designer in locating the cause of the occurrence of a deadlock. We first argue that the obvious approach to extract such sequences which is by sequential pattern mining and by contrasting patterns that are typical for the deadlocking counterexample traces but not typical for non-deadlocking traces, fails due to the inherent complexity of the problem. We then propose to extract substrings of specific length that only occur in the set of counterexamples for explaining the occurrence of deadlocks. We use a number of case studies to show the effectiveness of our approach and to compare it with an alternative approach to the counterexample explanation problem.