计算机工程与应用 ›› 2011, Vol. 47 ›› Issue (27): 98-101.

• 网络、通信、安全 • 上一篇    下一篇

采用NOP协议实现三模冗余系统的形式化验证

李婵娟1,周庆国2,崔向丽2   

  1. 1.兰州大学 数学与统计学院,兰州 730000
    2.兰州大学 信息科学与工程学院,兰州 730000
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2011-09-21 发布日期:2011-09-21

Using model checking for formal verification of TMR system based on NOP

LI Chanjuan1,ZHOU Qingguo2,CUI Xiangli2   

  1. 1.School of Mathematics and Statistics,Lanzhou University,Lanzhou 730000,China
    2.School of Information Science and Engineering,Lanzhou University,Lanzhou 730000,China
  • Received:1900-01-01 Revised:1900-01-01 Online:2011-09-21 Published:2011-09-21

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

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

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