On the use of a high-level fault model to check properties incompleteness
Franco Fummi, Graziano Pravadelli, A. Fedeli, Umberto Rossi, F. Toto · International Conference on Formal Methods and Models for Co-Design · 2003
The use of model checking to validate descriptions of digital systems lacks a coverage metrics. The set of proven properties can be incomplete, thus not guaranteeing the behavioral checking completeness of the digital system implementation with respect to the specification. This paper proposes a coverage methodology based on a combination of model checking, high-level fault simulation and automatic test pattern generation, to estimate the incompleteness of a set of formal properties. The adopted high-level fault model allows to join dynamic and formal verification.