Using model checking for formal verification of TMR system based on NOP
LI Chanjuan · Computer Engineering and Applications Journal · 2011
Fault tolerance is important for safety-critical systems.In order to minimize the common cause failure,the redundant elements are completely distributed,such as Triple Module Redundancy(TMR) system.In this paper,a new reliable broadcasting protocol-NOP is proposed to implement TMR fault-tolerant system in a distributed environment,which uses pre-defined sequence of nodes to solve the conflict of shared media.Under the assumption of a single fault,NOP can guarantee a orderly,reliable communication services.The correctness of protocol design is verified using model checking.The results show the triple modular redundancy system based on NOP can guarantee that under a single fault assumption,it can correctly detect and diagnose the faulty node and mask it,ensuring that all the normal nodes to maintain a consistent state,thus it can tolerate a single-fault.