loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03)
On the Use of a High-Level Fault Model to Check Properties Incompleteness
Mont Saint-Michel, France
June 24-June 26
ISBN: 0-7695-1923-7
ASCII Text
x 
 
Franco Fummi, Graziano Pravadelli, Andrea Fedeli, Umberto Rossi, Franco Toto, "On the Use of a High-Level Fault Model to Check Properties Incompleteness," Formal Methods and Models for Co-Design, ACM/IEEE International Conference on, pp. 145, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/MEMCOD.2003.1210099,
author = {Franco Fummi and Graziano Pravadelli and Andrea Fedeli and Umberto Rossi and Franco Toto},
title = {On the Use of a High-Level Fault Model to Check Properties Incompleteness},
journal ={Formal Methods and Models for Co-Design, ACM/IEEE International Conference on},
volume = {0},
year = {2003},
isbn = {0-7695-1923-7},
pages = {145},
doi = {http://doi.ieeecomputersociety.org/10.1109/MEMCOD.2003.1210099},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Formal Methods and Models for Co-Design, ACM/IEEE International Conference on
TI - On the Use of a High-Level Fault Model to Check Properties Incompleteness
SN - 0-7695-1923-7
SP
EP
A1 - Franco Fummi,
A1 - Graziano Pravadelli,
A1 - Andrea Fedeli,
A1 - Umberto Rossi,
A1 - Franco Toto,
PY - 2003
KW - null
VL - 0
JA - Formal Methods and Models for Co-Design, ACM/IEEE International Conference on
ER -
 
Franco Fummi, Universita di Verona
Graziano Pravadelli, Universita di Verona
Andrea Fedeli, STMicroelectronics
Umberto Rossi, STMicroelectronics
Franco Toto, STMicroelectronics
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.
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, pp.145, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03), 2003
Usage of this product signifies your acceptance of the Terms of Use.