NOP协议容错机制的设计与实现

作     者：闵蓉 

作者单位：兰州大学 

学位级别：硕士

导师姓名：周庆国

授予年度：2014年

学科分类：08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：安全关键系统 事件触发协议 容错协议 形式化验证 SPIN 

摘      要：NOP协议是针对小型安全关键实时系统开发的通信协议。该协议在深入分析现有通信协议的优缺点后,以功能安全理念为指导来设计与实现。NOP协议的主要特点是： (1)预先定义节点发送顺序,并在所有节点上达成共识,通信活动完全由事件本身触发。 (2)同时具备时间触发协议的可预测性和事件触发协议的灵活性特点。 (3)具有较高的网络利用率。 (4)协议的整个开发生命周期始终贯穿着功能安全理念。 本文在NOP协议的基础上进行改进,增加TMR+1容错机制,实现具有强容错的通信协议NOP V2.0。论文主要工作包括容错机制的设计、形式化验证及实现。在NOP V2.0设计和实现的整个生命周期中,始终贯穿了安全关键的理念,其以IEC61508安全标准作为指导,采用半形式化方法FMEA静态的、系统的分析容错协议的失效模式,并采用形式化验证工具SPIN动态的模拟了协议的运行状态,并对状态空间进行穷尽搜索,以检查协议是否发生了违反预期行为的情况。在形式化验证过程中,采用了状态约简技术,这种方法有效的减少了系统的状态空间规模,使得验证过程在较少的资源占用情况下达到预期的验证目标。验证结果表明NOP的容错、检错和故障诊断设计符合预期行为特性。在实现与测试阶段,本文采用wireshark网络封包分析软件对协议的通信活动进行了分析,结果说明协议的通信活动满足设计所要求的故障覆盖率要求。