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

【Abstract】 To increase the transmission rate and improve the redundancy structure design of the new generation Avionics 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 SkewMax 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.更多还原