CATALOGO DEI PRODOTTI DELLA RICERCA
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishLogical 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 |
File in questo prodotto:
http://hdl.handle.net/11562/23268
Copyright © 2021