Formal verification of signature monitoring mechanisms using model checking

In recent decades, reliability in the presence of transient faults is already a significant problem for concern. To mitigate the effects of such faults, fault-tolerant techniques are proposed. However, validating the effectiveness of such fault-tolerant techniques constitutes another problem. In this paper, we put forward an original approach to evaluate the effectiveness of signature monitoring mechanisms. It is based on model checking principles. Firstly, the program strengthened by signature monitoring algorithm is modeled as a state transition system. Then a translation procedure is proposed to describe how to translate the state transition system into the input program of model checker NuSMV. By NuSMV, two reprehensive signature monitoring algorithms are verified. The verification results reveal some undetected errors which have not been found before.