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

Model Checking of Credit Setting in AFDX Traffic Policing

作　　者：高宇[1] 李峭[2] 熊华钢[2] 

机构地区：[1]北京航空航天大学中法工程师学院,北京100191 [2]北京航空航天大学电子信息工程学院,北京100191

出　　处：《航空计算技术》2011年第3期122-126,134,共6页Aeronautical Computing Technique

基　　金：国家自然科学基金项目资助(61073012);航空科学基金项目资助(20081951028)

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

关 键 词：AFDX 时延抖动 信用量令牌桶 时间自动机 模型检查 

分 类 号：TP393.03[自动化与计算机技术—计算机应用技术]