1Premiers resultats sur l’utilisation d’ACL2 pour l’evaluation de la consequence des erreurs logiques
Renaud Clavel, Laurence Pierre, Régis Leveugle · 2008
Abstract—Nous nous proposons de développer de nouvelles méthodologies, basées sur une combinaison de techniques d’injection de fautes et de méthodes formelles, pour l’analyse de la robustesse d’un circuit décrit au niveau RTL, vis a ̀ vis des erreurs créées par des fautes transitoires. Nous présentons ici nos premiers résultats quant a ̀ l’utilisation du démonstrateur de théorèmes ACL2, dans le contexte de systèmes avec dispositif de correction. I. INTRODUCTION- CONTEXTE La conception de circuits fiables nécessite en particulier de pouvoir évaluer, a ̀ chacune de ses étapes, le niveau de robustesse atteint vis a ̀ vis de divers types de fautes ou d’erreurs [1]. Dans les systèmes critiques (aéronautique et