AFDX流量管制信用量设置的模型检查

航空电子全双工交换式以太网（AFDX）实时通信中,交换节点采用信用量令牌桶（creditedtoken bucket）进行流量管制。分别对基于帧和基于字节的信用量令牌桶流量管制进行时间自动机建模,并构建模型的并发交互场景;采用测试自动机,进行有界活性（bounded liveness）模型检查。通过形式化验证,发现流量管制通过约束突发度限制多路复用输出排队的时延抖动,但信用量值的设置必须考虑输入虚拟链路（VL）的时延抖动,否则可能导致已经聚合的流量中属于不同VL的帧的先后次序被破坏,反而造成更大的时延抖动。通过分析时延抖动对信用量设置的影响,归纳并给出流量管制信用量设置的注意事项。

Model Checking of Credit Setting in AFDX Traffic Policing

In the Avionics Full Duplex Switched Ethernet(AFDX) real-time communications,credited token buckets are applied in switched nodes for traffic policing.Test automata are designed for bounded liveness model checking under concurrent interaction scenarios with the time automata models,which are built for the frame-based and byte-based credited token buckets respectively.According to the formal verification,it′s shown that latency jitters in multiplexer output queuing are limited by traffic policing with burstiness constraints.However,jitters of input virtual links(VL) should also be considered when setting the credit values;otherwise,the greater jitter values may be caused by disturbing aggregated frames belong to different VLs.By analyzing the inter-relations of credit setting and jitters,some notes are summarized for traffic policing configurations.