A Practical Approach to Coverage in Model Checking

Hana Chockler, Orna Kupferman, Robert Kurshan, Moshe Y. Vardi

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

76 Citations (Scopus)

Abstract

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 implemented on top of existing model checking tools.
Original languageEnglish
Title of host publicationComputer Aided Verification, 13th International Conference (CAV)
Place of PublicationParis
PublisherSpringer
Pages66-78
Volume2102
Publication statusPublished - 2001

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume2102

Fingerprint

Dive into the research topics of 'A Practical Approach to Coverage in Model Checking'. Together they form a unique fingerprint.

Cite this