Logical consequence between properties is generally examined by using theorem proving, which may require a large amount of time and space resources. This paper proposes a faster approach, which analyzes logical consequences by observing the property capability of revealing high-level faults. We consider a set of properties defined to check the correctness of a design (DUV) with respect to the specification. The paper proves that if there is only one property that distinguishes between a faulty and a fault-free behavior of the DUV, and then it cannot be a logical consequence of the remaining properties. It is shown that the reverse implication of such a theorem depends on the selected high-level fault model. According to these theoretical results, the paper proposes a method to analyze logical consequence of properties based on high-level fault simulation and theorem proving.

On the Use of a High-Level Fault Model to Analyze Logical Consequence of Properties

FUMMI, Franco;PRAVADELLI, Graziano
2005

Abstract

Logical consequence between properties is generally examined by using theorem proving, which may require a large amount of time and space resources. This paper proposes a faster approach, which analyzes logical consequences by observing the property capability of revealing high-level faults. We consider a set of properties defined to check the correctness of a design (DUV) with respect to the specification. The paper proves that if there is only one property that distinguishes between a faulty and a fault-free behavior of the DUV, and then it cannot be a logical consequence of the remaining properties. It is shown that the reverse implication of such a theorem depends on the selected high-level fault model. According to these theoretical results, the paper proposes a method to analyze logical consequence of properties based on high-level fault simulation and theorem proving.
0780392272
Fault model; Property optimization
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/23268
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 0
social impact