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

作者：罗泽雄; 高驰; 吴伯春; 汤雪乾; 许伟钰; 曲国远; 徐晓飞

来源：航空电子技术, 2023, 54(01): 1-8.

DOI：10.12175/j.issn.1006-141X.2023.01.01

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

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

• 单位
  中国航空无线电电子研究所; 华东师范大学; 成都飞机设计研究所