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

• 作者: 李峭 熊华钢 高宇
• 来源期刊: 航空计算技术
• 关键词: AFDX 时延抖动 信用量令牌桶 时间自动机 模型检查
• 年，卷（期）: 2011,（3）
• 所属期刊栏目: 计算机网络
• 页码范围: 122-126,134
• 分类号: TP393.03
• 语种: 中文
• DOI: 10.3969/j.issn.1671-654X.2011.03.032

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	熊华钢	北京航空航天大学电子信息工程学院	179	1571	21.0	31.0
2	高宇	北京航空航天大学中法工程师范学院	3	11	2.0	3.0
3	李峭	北京航空航天大学电子信息工程学院	71	353	9.0	17.0