A Practical Approach to Coverage in Model Checking

Hana Chockler, Orna Kupferman, Robert Kurshan, Moshe Vardi

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


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.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems