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

An AADL end-to-end flow specification verification method based on timed automata

作　　者：白先平 姚袭欣 陈香兰 刘翀 李曦[1] BAI Xian-ping;YAO Xi-xin;CHEN Xiang-lan;LIU Chong;LI Xi(School of Software Engineering,University of Science and Technology of China,Hefei 230026,China)

机构地区：[1]中国科学技术大学软件学院,安徽合肥230026

出　　处：《计算机工程与科学》2023年第5期810-819,共10页Computer Engineering & Science

基　　金：国家自然科学基金(61772482)。

摘　　要：体系结构分析及设计语言(AADL)作为一种标准且直观的实时系统分析与设计工具,可以为系统设计、分析、验证、自动代码生成等关键环节提供统一的抽象表示。然而,AADL模型采用仿真的验证方法无法得到精确的端到端延迟验证结果,尤其是对于资源动态分配的实时系统。为解决结果不精确的问题,可结合基于系统有穷状态空间遍历的模型检验方法。首先,将实时系统AADL模型转换为时间自动机(TA)模型,以TA为理论体系进行模型检验。其次,基于反应链的需求分类定义端到端延迟需求表达模式。最后,给出对应需求模式的观察者模型,与系统模型并行组合,优化模型验证的时空资源消耗。Architecture analysis and design language(AADL)is a standard and intuitive real-time system design tool,which provides uniform standards for key steps such as model design,analysis,verification,and automatic code generation.However,using simulation,the verification method of AADL model cannot obtain accurate results of end-to-end flow,especially for real-time systems with dynamic resource allocation.To solve this problem of inaccurate results,AADL is combined with the model checking method to traverse the system􀆳s infinite state space.Firstly,the AADL model of the real-time system is converted into a timed automata(TA)model,and the TA is used as the theoretical system for model checking verification.Secondly,the pattern of end-to-end delay requirements is defined,based on the demand classification of the response chain.Finally,the corresponding observer model is implemented according to the pattern and combined with the system model in parallel to reduce the time as well as space resources consumed by the verification algorithm.

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

分 类 号：TP391.41[自动化与计算机技术—计算机应用技术]