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

作     者：符宁 杜承烈 李建良 刘志强 彭寒 Fu Ning;Du Chenglie;Li Jianliang;Liu Zhiqiang;Peng Han

作者机构：西北工业大学计算机学院西安710072 西北农林科技大学信息工程学院陕西杨凌712100 西北工业大学软件学院西安710072 西安航空学院计算机工程系西安710077 

基　　金：国家"八六三"高技术研究发展计划基金项目(2011AA010102) 中国航空科学基金项目(20115553023) 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2015年第52卷第1期

页      码：167-176页

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

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

学科分类：0810[工学-土木类] 0808[工学-自动化类] 0839[0839] 08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.7544/issn1000-1239.2015.20130722

馆 藏 号：203464167...