In formal verification, we verify that a system is correct with
respect to a specification. When verification succeeds and the system
is proven to be correct, there is still a question of how complete the
specification is, and whether it really covers all the behaviors of
the system. In this paper we study coverage metrics for model
checking from a practical point of view. Coverage metrics are based
on modifications we apply to the system in order to check which parts
of it were actually relevant for the verification process to succeed.
We suggest several definitions of coverage, suitable for
specifications given in linear temporal logic or by automata on
infinite words. We describe two algorithms for computing the parts of
the system that are not covered by the specification. The first
algorithm is built on top of automata-based model-checking
algorithms. The second algorithm reduces the coverage problem to the
model-checking problem. Both algorithms can be easily implemented on
top of existing model checking tools. In addition, we study the
possibility of extracting coverage information about the system by
examining its quotient abstraction.
