Some Logical Conditions and Probabilistic Characteristics as a Guide for Fault-Tolerant Systems Verification

In this paper we consider a way of using both formal-logical and probabilistic models based on Finite State Machine (FSM) for semi-automatic verification of fault tolerant properties and Soft Error robustness of a target design. This verification is based on some numerical characteristics of the FSM behavior which can be used to identify latches/registers that must be protected against some transient faults in order to satisfy a formal specification. Such combination of formal verification with analysis of fault-tolerant property could reduce overall design cost, what can increase considerably the formal verification tools effectiveness.