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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
