Transition traversal coverage estimation for symbolic model checking
Transition traversal coverage estimation for symbolic model checking
复制标题
DOI：
10.1109/icasic.2005.1611460
复制
发表时间：
2005-12
期刊：
影响因子：
--
通讯作者：
Xingwen Xu;Shinji Kimura;K. Horikawa;T. Tsuchiya
中科院分区：
文献类型：
--
作者：
Xingwen Xu;Shinji Kimura;K. Horikawa;T. Tsuchiya
模型检查可以详尽地验证给定实现上的一组指定属性。然而，很难确定是否已经指定了足够的属性。在本文中，我们提出了一个过渡遍历覆盖的CTL子集的性质的完整性评估方法。利用这种方法，我们可以检测到没有任何属性验证的转换。它比基于状态的覆盖度量更全面和准确。我们避免产生的扰动实现直接遍历的基础上的CTL公式的语义转换。实验结果表明，该方法能够以较低的计算代价发现细微的覆盖漏洞。
Model checking can exhaustively verify a set of specified properties on a given implementation. However, it is very hard to determine whether sufficient properties have been specified or not. In this paper, we propose a transition traversal coverage method for a subset of CTL to evaluate the completeness of properties. With this method, we can detect the transitions which are not verified by any property. It is more comprehensive and accurate than state-based coverage metric. We avoid generating the perturbed implementation by directly traversing transitions based on the semantics of CTL formulas. Experimental results show that the proposed method can discover subtle coverage holes with low computation cost.