时间触发以太网拜占庭容错方法的形式化验证

对于时间触发以太网的拜占庭容错方法,已有的推理性论证表明网络的分布式时钟同步机制有利于容错过程中实现交互一致性。为对该容错方法的正确性进行严格验证,进一步采用模型检查的形式化分析手段,通过符号分析实验室(SAL)形式化工具,构建了网络节点模型,建立了时间触发体系结构下的拜占庭容错场景,设定了容错操作活性、一致性和有效性等属性的形式化定理。模型检查的结果表明:在三冗余独立路径条件下,该方法可以容忍一个拜占庭故障,且在存在指令/监视对(COM/MON pair)的条件下可以容忍2个高完整性配置节点的"不一致遗漏"故障。与推理论证手段相比,SAL模型检查为时间触发交换式网络在航空航天高安全关键等级系统中的容错配置提供了更规范的依据。     

基于重要性抽样的时间触发调度表生成方法

时间触发以太网(TTE)是分布式综合模块化航空电子(DIMA)系统互连中的骨干网络，需要生成无冲突的时间触发(TT)流量调度表。形式化SMT求解可以抽象地表述多种调度约束；但TT流量间，以及TT流量与分区调度之间存在作业链依赖关系，较复杂的约束会降低求解器的效率。将重要性抽样(IS)方法应用于TT调度表的启发式求解，通过统计“尽可能快”(ASAP)求解的尝试偏移量的经验分布，扭转该变量的抽样分布进行迭代寻优；并针对调度的可行性及作业链的及时性，将IS求解分为2个阶段进行。案例研究表明：第1阶段的IS会演化得出易于保证严格周期调度或抖动较小的尝试偏移量分布，第2阶段IS则会进一步根据作业链的最坏总延迟最小准则进行迭代优化，并且对于分区调度与TT流量调度存在或不存在同步关系的场景都具有适用性。     

千兆三余度AFDX 帧管理的形式化建模与验证

为了提升新一代航空电子全双工交换以太网（AFDX）网络的传输速率和余度设计可靠性，在AFDX 网络标准的基础上（ARINC 664 p7），建立千兆三余度AFDX 网络的帧管理机制模型并进行了形式化建模， 而且实现了AFDX 网络标准中描述的SkewMax 机制。使用UPPAAL 形式化工具对千兆三余度AFDX 网络帧 管理机制进行形式化验证，验证帧管理机制的完整性检查及冗余管理功能的可用性。结果表明，千兆三余度 AFDX 网络帧传输过程中不存在死锁。此外，针对标准AFDX 的冗余管理中一个帧的丢失可能会导致其冗余备 份的丢失的现象，提出在接收端设置一个队列，记录那些比连续帧更晚到达的冗余备份的帧序号，从而减少不 必要的丢帧，提高QoS 和数据完整性。形式化验证的结果可以作为千兆AFDX 网络标准制定和实际应用的参考。