| Abstract |
|
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.
|
 Additional Information
|
Citation:
Franco Fummi, Graziano Pravadelli, Andrea Fedeli, Umberto Rossi, Franco Toto,
"On the Use of a High-Level Fault Model to Check Properties Incompleteness,"
memocode,
p. 145,
First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE’03),
2003
|
