Feasibility analysis for robustness quantification by symbolic model checking

We propose and investigate a robustness evaluation procedure for sequential circuits subject to particle strikes inducing bit-flips in memory elements. We define a general fault model, a parametric reparation model and quantitative measures reflecting the robustness capability of the circuit with respect to these fault and reparation models. We provide algorithms to compute these metrics and show how they can be interpreted in order to better understand the robustness capability of several circuits (a simple circuit coming from the VIS distribution, circuits from the itc-99 benchmarks and a CAN-Bus interface).