Extended abstract: transition traversal coverage estimation for symbolic model checking

Model checking can exhaustively verify whether a system (implementation) satisfies a set of properties (formal specification). However, the completeness of the formal specification itself is not clear and needs to be evaluated. Several coverage estimation methods have been proposed for this issue. In this paper, we present a transition traversal coverage method for a subset of CTL. With this method, we can detect the transitions, which are not verified by any property. It is more accurate and comprehensive than the state coverage method.