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

来源：计算机工程与科学杂志2023年第5期北京时间：

作者：白先平, 姚袭欣, 陈香兰, 刘翀, 李曦

单位：（中国科学技术大学软件学院，安徽 合肥 230026）

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

关键词：实时系统验证,AADL,时间自动机,观察者,

基金资助：国家自然科学基金（61772482）