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

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

来源：Z201501018, 2015, (01): 167-176.

• 复杂嵌入式实时系统
• 体系结构分析设计语言
• UPPAAL
• 可调度性
• 模型检测 complex embedded real-time system
• architecture analysis and design language(AADL)
• UPPAAL
• schedulability analysis
• model checking

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

• 出版日期2015
• 单位西安航空学院; 西北工业大学; 西北农林科技大学