Towards robustness analysis using PVS

Abstract

This work targets the use of formal methods for enhancing dependability analysis of sequential circuits described at the Register Transfer (RT) level. We consider solutions oriented towards theorem-proving techniques as an alternative to classical fault-injection techniques, for analyzing the consequences of errors caused by transient faults. A preliminary study was conducted to evaluate the advantages of a highly automated tool like ACL2 in that context. However, this study showed that, in spite of its numerous advantages, the ACL2 logic is not always expressive enough to deal with the properties under consideration here. In this paper, we briefly explain the shortcomings of ACL2 relatively to our problem, and we investigate the application of PVS, thus enabling to improve our simple and multiple faults models and the associated verification methodology. © 2011 Springer-Verlag.