论文部分内容阅读
航空电子全双工交换式以太网(AFDX)实时通信中,交换节点采用信用量令牌桶(creditedtoken bucket)进行流量管制。分别对基于帧和基于字节的信用量令牌桶流量管制进行时间自动机建模,并构建模型的并发交互场景;采用测试自动机,进行有界活性(bounded liveness)模型检查。通过形式化验证,发现流量管制通过约束突发度限制多路复用输出排队的时延抖动,但信用量值的设置必须考虑输入虚拟链路(VL)的时延抖动,否则可能导致已经聚合的流量中属于不同VL的帧的先后次序被破坏,反而造成更大的时延抖动。通过分析时延抖动对信用量设置的影响,归纳并给出流量管制信用量设置的注意事项。
In avionics full-duplex switched Ethernet (AFDX) real-time communications, switching nodes use a credited token bucket for traffic control. The time automata was modeled based on the flow control of frame and byte-based credit token bucket, and the concurrent interaction scenario of the model was constructed. The bounded liveness model was checked by using test automaton. Through formal verification, it is found that traffic regulation limits the delay jitter of multiplexed output queues by constraining burstiness, but the setting of credit value must take into account the delay jitter of the input virtual link (VL), which may lead to aggregation The order of the frames belonging to different VLs in the traffic of the traffic is destroyed, which leads to greater delay jitter. By analyzing the influence of delay jitter on credit setting, the precautions of setting credit limit of the traffic control are summarized and given.