< retour aux publications

ACL2 for the Verification of Fault-Tolerance Properties: First Results

Auteur(s) : L. Pierre, R. Clavel, R. Leveugle

Doc. Source: International Workshop on The ACL2 Theorem Prover and Its Applications

Publisher : ACM, NY, USA

Pages : 90-99

We target the development of new methodologies for analyzing the robustness of circuits described at the Register Transfer (RT) level, with respect to errors caused by transient faults. Analyzing the potential consequences of errors usually involves fault-injection techniques, using simulation or emulation-based solutions. Our goal is to take advantage of the logical power of theorem proving tools to get alternative solutions that would allow to reason purely symbolically on errors. In this paper we present our preliminary results with the ACL2 theorem prover, in the context of devices that have auto-correction features. First we give a logical definition of the error model as a conjunction of characteristic properties, from which robustness analysis can be performed. Then we improve the methodology to deal with hierarchical systems.