| 采用NOP协议实现三模冗余系统的形式化验证 |
| |
| 引用本文： | 李婵娟,周庆国,崔向丽.采用NOP协议实现三模冗余系统的形式化验证[J].计算机工程与应用,2011,47(27):98-101. |
| |
| 作者姓名： | 李婵娟 周庆国 崔向丽 |
| |
| 作者单位： | 1.兰州大学 数学与统计学院，兰州 7300002.兰州大学 信息科学与工程学院，兰州 730000 |
| |
| 基金项目： | 国家自然科学基金(No.60973137); 甘肃省科技计划(No.090WC-GA891); 中央高校基本科研业务费专项资金资助(No.lzujbky-2010-89)~~ |
| |
| 摘 要： | 对于安全关键系统容错是其实现安全性的重要手段，为最小化冗余单元之间的关联性，通常采用分布式冗余系统，典型的是三模冗余系统。为了在分布式环境下，实现基于三模冗余机制的容错系统，提出了一种可靠的广播协议-NOP（Node Order Protocol），它采用预定义的节点顺序解决共享介质冲突，并且在单一故障模式假设下，实现了有序的、可靠的消息传输服务，并采用基于模型检测的形式化方法进行了容错系统安全性的验证。验证结果显示基于NOP协议构建的三模冗余系统，在单一任意故障模式下，能够正确地进行故障的检测和诊断，并保证所有正常节点保持一致状态，从而保证单一故障节点被掩蔽，实现单一故障的容错能力。
|
| 关 键 词： | 节点顺序协议 容错 三模冗余 模型检测 |
| 修稿时间： | |
Using model checking for formal verification of TMR system based on NOP |
| |
| LI Chanjuan,ZHOU Qingguo,CUI Xiangli.Using model checking for formal verification of TMR system based on NOP[J].Computer Engineering and Applications,2011,47(27):98-101. |
| |
| Authors: | LI Chanjuan ZHOU Qingguo CUI Xiangli |
| |
| Affiliation: | 1.School of Mathematics and Statistics，Lanzhou University，Lanzhou 730000，China2.School of Information Science and Engineering，Lanzhou University，Lanzhou 730000，China |
| |
| 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.T... |
| |
| Keywords: | node order protocol fault-tolerance triple modular redundancy model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
