Abstract: 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.

Key words: node order protocol, fault-tolerance, triple modular redundancy, model checking

摘要： 对于安全关键系统容错是其实现安全性的重要手段，为最小化冗余单元之间的关联性，通常采用分布式冗余系统，典型的是三模冗余系统。为了在分布式环境下，实现基于三模冗余机制的容错系统，提出了一种可靠的广播协议-NOP（Node Order Protocol），它采用预定义的节点顺序解决共享介质冲突，并且在单一故障模式假设下，实现了有序的、可靠的消息传输服务，并采用基于模型检测的形式化方法进行了容错系统安全性的验证。验证结果显示基于NOP协议构建的三模冗余系统，在单一任意故障模式下，能够正确地进行故障的检测和诊断，并保证所有正常节点保持一致状态，从而保证单一故障节点被掩蔽，实现单一故障的容错能力。

关键词: 节点顺序协议, 容错, 三模冗余, 模型检测