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

• 作者: 周庆国 崔向丽 李婵娟
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 节点顺序协议:容错 三模冗余 模型检测
• 年，卷（期）: 2011,（27）
• 所属期刊栏目: 网络、通信、安全
• 页码范围: 98-101,106
• 分类号: TP31
• 字数: 6408字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2011.27.027

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周庆国	兰州大学信息科学与工程学院	41	278	8.0	15.0
2	李婵娟	兰州大学数学与统计学院	3	7	2.0	2.0
3	崔向丽	兰州大学信息科学与工程学院	1	1	1.0	1.0