Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking
Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking
复制标题
DOI：
10.1109/tse.2009.57
复制
发表时间：
2010-01-01
影响因子：
7.4
通讯作者：
Leue, Stefan
中科院分区：
文献类型：
--
作者：
Aljazzar, Husain;Leue, Stefan
当前的随机模型检查器不容易使反例的财产侵犯。在本文中，我们应用直接显式状态空间搜索离散和连续时间马尔可夫链，以计算违反PCTL或CSL性质的反例。定向显式状态空间搜索算法探索状态空间的飞行，这使得我们的方法非常有效和高度可扩展。它们也可以使用通常可以提高该方法的性能的方法学来指导。我们的方法提供的反例有两个重要的属性。首先，它们包括那些对财产侵犯贡献最大可能性的痕迹。因此，它们显示了系统中最可能的违规执行场景。第二，得到的反例往往是小的。因此，它们可以由人类用户有效地分析。这两个属性使我们的方法得到的反例非常有用的调试目的。我们实现了我们的方法的基础上随机模型检查PRISM，并将其应用到一些案例研究，以说明其适用性。
Current stochastic model checkers do not make counterexamples for property violations readily available. In this paper, we apply directed explicit state-space search to discrete and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties. Directed explicit state-space search algorithms explore the state space on-the-fly, which makes our method very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method. Counterexamples provided by our method have two important properties. First, they include those traces which contribute the greatest amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes. We implemented our method based on the stochastic model checker PRISM and applied it to a number of case studies in order to illustrate its applicability.