AADL分级调度模型的分析与验证

来源：计算机研究与发展杂志2015年第1期北京时间：

作者：符宁,杜承烈,李建良,刘志强,彭寒,

摘要：针对嵌入式系统体系结构分析设计语言(architectureanalysisanddesignlanguage,AADL)分级调度模型的分析问题,提出了基于模型检验的可调度性分析和验证方法.基于时间自动机理论，将AADL分级调度模型转换为时间自动机网络，将待验证性质描述为时序逻辑公式，通过模型检验工具对可调度性进行分析和验证.研究结果表明，使用模型检验方法来分析AADL分级调度模型的可调度性是可行的.相对其他方法而言,该方法利用了形式化方法的穷举性来分析系统的性质,分析结果更加精确.

关键词：复杂嵌入式实时系统, 体系结构分析设计语言, UPPAAL, 可调度性, 模型检测,