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

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