On the use of model checking for the verification of a dynamic signature monitoring approach

Consequences of transient faults represent a significant problem for today´s electronic circuits and systems. As the probability of such errors increases, incorporation of error detection and correction mechanisms is mandatory. It is well known that traditional techniques that validate system´s reliability do not cover the whole spectrum of fault scenarios, because fault models are linked to target architectures. Therefore, validating the completeness of robust fault tolerance techniques is a major issue when assessing reliability improvements these techniques can produce. In this paper, we propose an original approach to evaluate the system reliability with respect to Single Event Upset (SEU) errors. It is based on model-checking principles. In addition, a signature analysis technique is evaluated. This technique was previously validated using a simulation-based fault injection approach. Simulation results showed that no error escapes detection. However, simulation based fault injection cannot guarantee that all fault consequences have been investigated. This limitation motivates us to explore a formal verification approach that targets a complete validation. Model checking has a fundamental advantage over classic fault-injection techniques: it can cover all possible SEU fault scenarios from a predefined class. Results reported in this paper demonstrate the efficiency of this validation approach over usual simulation-based techniques.