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

摘要： 体系结构分析及设计语言(AADL)作为一种标准且直观的实时系统分析与设计工具，可以为系统设计、分析、验证、自动代码生成等关键环节提供统一的抽象表示。然而，AADL模型采用仿真的验证方法无法得到精确的端到端延迟验证结果，尤其是对于资源动态分配的实时系统。为解决结果不精确的问题，可结合基于系统有穷状态空间遍历的模型检验方法。首先，将实时系统AADL模型转换为时间自动机(TA)模型，... （共10页）