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

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

基于UPPAAL软件的实时系统设计研究

UPPAAL是丹麦Aalborg和瑞士Uppsala大学联合开发,具有世界先进水平的实时系统模拟,校核的软件,基于对实时系统严密逻辑,真实时间的抽象,而构建时间状态机动态模型网络,模拟,校核系统,检测潜在失败,保证设计可靠性,雷达传感器内存接口实时系统是航天雷达系统重要组成部分。本文UPPAAL软件对此系统精确的动态数学模型,模拟,校核系统,覆盖各设计阶段,保证实时系统设计可靠性。