Transition traversal coverage estimation for symbolic model checking

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.