基于时间自动机的AADL端到端流规约验证方法

体系结构分析及设计语言(AADL)作为一种标准且直观的实时系统分析与设计工具,可以为系统设计、分析、验证、自动代码生成等关键环节提供统一的抽象表示.然而,AADL模型采用仿真的验证方法无法得到精确的端到端延迟验证结果,尤其是对于资源动态分配的实时系统.为解决结果不精确的问题,可结合基于系统有穷状态空间遍历的模型检验方法.首先,将实时系统AADL模型转换为时间自动机(TA)模型,以TA为理论体系进行模型检验.其次,基于反应链的需求分类定义端到端延迟需求表达模式.最后,给出对应需求模式的观察者模型,与系统模型并行组合,优化模型验证的时空资源消耗.