On the Use of a High-Level Fault Model to Check Properties Incompleteness

The use of model checking to validate descriptions ofdigital systems lacks a coverage metrics. The set of provenproperties can be incomplete, thus not guaranteeing the behavioralchecking completeness of the digital system implementationwith respect to the specification. This paper proposesa coverage...

Full description

Saved in:
Bibliographic Details
Main Authors: Fummi, Franco, Pravadelli, Graziano, Fedeli, Andrea, Rossi, Umberto, Toto, Franco
Format: Conference Proceeding
Language:English
Subjects:
General and reference > Cross-computing tools and techniques > Reliability
Software and its engineering > Software creation and management > Software verification and validation > Process validation
Software and its engineering > Software organization and properties > Extra-functional properties > Software reliability
Software and its engineering > Software organization and properties > Software functional properties > Formal methods > Model checking
Theory of computation > Logic > Verification by model checking
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The use of model checking to validate descriptions ofdigital systems lacks a coverage metrics. The set of provenproperties can be incomplete, thus not guaranteeing the behavioralchecking completeness of the digital system implementationwith respect to the specification. This paper proposesa coverage methodology based on a combination ofmodel checking, high-level fault simulation and automatictest pattern generation, to estimate the incompleteness of aset of formal properties. The adopted high-level fault modelallows to join dynamic and formal verification.
DOI:10.5555/823453.823844