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

Formal Modeling and Verification of the Gigabit Triple Redundancy AFDX Frame Management

作　　者：罗泽雄[1] 高驰 吴伯春[1] 汤雪乾 许伟钰 曲国远[1] 徐晓飞[1] LUO Ze-xiong;GAO Chi;WU Bo-chun;TANG Xue-qian;XU Wei-yu;QU Guo-yuan;XU Xiao-fei(China Aeronautical Radio Electronics Research Institute,Shanghai 200233,China;Chengdu Aircraft Design&Research Institute,Chengdu 610073,China;East China Normal University,Shanghai 200061,China)

机构地区：[1]中国航空无线电电子研究所,上海200233 [2]成都飞机设计研究所,成都610073 [3]华东师范大学,上海200061

出　　处：《航空电子技术》2023年第1期1-8,共8页Avionics Technology

摘　　要：为了提升新一代航空电子全双工交换以太网(AFDX)网络的传输速率和余度设计可靠性,在AFDX网络标准的基础上(ARINC 664 p7),建立千兆三余度AFDX网络的帧管理机制模型并进行了形式化建模,而且实现了AFDX网络标准中描述的SkewMax机制。使用UPPAAL形式化工具对千兆三余度AFDX网络帧管理机制进行形式化验证,验证帧管理机制的完整性检查及冗余管理功能的可用性。结果表明,千兆三余度AFDX网络帧传输过程中不存在死锁。此外,针对标准AFDX的冗余管理中一个帧的丢失可能会导致其冗余备份的丢失的现象,提出在接收端设置一个队列,记录那些比连续帧更晚到达的冗余备份的帧序号,从而减少不必要的丢帧,提高QoS和数据完整性。形式化验证的结果可以作为千兆AFDX网络标准制定和实际应用的参考。To increase the transmission rate and improve the redundancy structure design of the new generation Avi-onics Full-Duplex Switched Ethernet(AFDX)network,a formal modeling of the frame management mechanism of the gigabit triple redundancy AFDX is established based on the AFDX network standard(ARINC 664 p7)and the Skew-Max mechanism described in the AFDX network standard is implemented.The availability of the integrity check and redundancy management functions is verified by UPPAAL formal tool.The verification results show that there is no deadlock in the frame transmission process in this design.The AFDX design document mentions that the loss of a frame in redundancy management may lead to the loss of its redundant backup.For this,a queue is recommended to be setup at the receiving end-system to record those frame sequence numbers of redundant backup frames that arrive later than consecutive frames,thereby reducing unnecessary frame retransmission and improving QoS and data integrity.The results of formal verification can be used as a reference for the formulation and practical application of gigabit AFDX network standards.

关 键 词：千兆AFDX 三余度 帧管理设计 形式化建模 完整性检查 冗余管理 

分 类 号：V247.1[航空宇航科学与技术—飞行器设计] TP393.1[自动化与计算机技术—计算机应用技术]