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.
Titolo: | On the Use of a High-Level Fault Model to Analyze Logical Consequence of Properties |
Autori: | |
Data di pubblicazione: | 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. |
Handle: | http://hdl.handle.net/11562/23268 |
ISBN: | 0780392272 |
Appare nelle tipologie: | 04.01 Contributo in atti di convegno |