● 摘要
航空电子全双工交换式以太网（Avionics Full-Duplex Switched Ethernet，AFDX）是先进的大中型飞机的综合化航空电子互连网络，AFDX网络实时通信中，需要考虑数据因链路抢占和流量管制导致的时延抖动。时间自动机（Time Automata, TA）是一种基于模型的形式化方法，并可以结合模型检查（Model Checking）技术进行形式化验证。本文所述的研究工作采用时间自动机对AFDX网络的端系统（End System，ES）进行建模，给出AFDX端系统信号发送、虚拟链路组装、多路复用排队等行为的时间自动机模型，构建模型的并发交互场景，对ES的流量整形、流量及其实时通信的行为进行模型检查和在线（on-line）测试。经过研究和实验，得到如下具有新颖性的研究成果： 应用时间自动机建模和模型检查方法验证端到端传输中“突发一次性”原则，得出了AFDX网络流量适用于这一原则的结论； 建立了AFDX端系统和交换节点模型并发交互的场景，该场景不局限于基于帧（frame-based）的流量整形，而且包括需要考虑信用量（credit token）数值的基于字节（byte-based）的令牌桶（token bucket）流量整形，考虑了不同长度帧进行变长时间处理与相应类型的设置，得出了AFDX流量管制机制对时延抖动影响的实验检验结果，归纳并给出了流量管制信用量设置的注意事项。 结合在线测试技术在时间自动机模型检查中的应用，通过将引擎模型中的信号量与虚拟以太网卡的驱动信号建立联系，实现了测试引擎与AFDX端系统模型的互操作。