Coverage estimation for symbolic model checking
Yatin Hoskote, Timothy Kam, Pei-Hsin Ho, Xudong Zhao · 1999
Although model checking is an exhaustive formal verification method, a bug can still escape detection if the erroneous behavior does not violate any verified property.We propose a coverage metric to estimate the "completeness" of a set of properties verified by model checking.A symbolic algorithm is presented to compute this metric for a subset of the CTL property specification language.It has the same order of computational complexity as a model checking algorithm.Our coverage estimator has been applied in the course of some real-world model checking projects.We uncovered several coverage holes including one that eventually led to the discovery of a bug that escaped the initial model checking effort.