Formal Analysis of Fault Propagation in Complex Digital Systems

From bibtex.

Abstract

With the increasing availability of computational resources and the progress in research concerning automated formal methods, the characterization of safety features for hardware requires improved precision in functional vulnerability detection. In the context of formal fault injection, the model checking algorithm can be used to detect vulnerabilities in digital systems by violating the nominal temporal properties. We present a general methodology to reduce the state space that is computed and traversed during these fault campaigns. The chosen criteria preserves the nominal behavior and the failure modes, expressed by the fault-violated properties. This process is crucial to provide a manipulable object for subsequent Failure Mode and Effects Analysis. Finally, we propose an assumption-based guarantee technique to model how a fault may propagate through different hardware units, for a scalable methodology of formal fault injection and vulnerability detection in complex SoCs.