|
|||||
|
|
| AADL分级调度模型的分析与验证 | |
| 引用本文： | 符宁,杜承烈,李建良,刘志强,彭寒.AADL分级调度模型的分析与验证[J].计算机研究与发展,2015,52(1). |
| 作者姓名： | 符宁 杜承烈 李建良 刘志强 彭寒 |
| 作者单位： | 1. 西北工业大学计算机学院 西安 710072 2. 西北农林科技大学信息工程学院 陕西杨凌712100 3. 西北工业大学软件学院 西安 710072 4. 西安航空学院计算机工程系 西安 710077 |
| 基金项目： | 国家“八六三”高技术研究发展计划基金项目，中国航空科学基金项目 |
| 摘 要： | 针对嵌入式系统体系结构分析设计语言(architecture analysis and design language,AADL)分级调度模型的分析问题,提出了基于模型检验的可调度性分析和验证方法.基于时间自动机理论,将AADL分级调度模型转换为时间自动机网络,将待验证性质描述为时序逻辑公式,通过模型检验工具对可调度性进行分析和验证.研究结果表明,使用模型检验方法来分析AADL分级调度模型的可调度性是可行的.相对其他方法而言,该方法利用了形式化方法的穷举性来分析系统的性质,分析结果更加精确. |
| 关 键 词： | 复杂嵌入式实时系统 体系结构分析设计语言 UPPAAL 可调度性 模型检测 |
Analysis and Verification of AADL Hierarchical Schedulers |
|
| Fu Ning,Du Chenglie,Li Jianliang,Liu Zhiqiang,Peng Han.Analysis and Verification of AADL Hierarchical Schedulers[J].Journal of Computer Research and Development,2015,52(1). | |
| Authors: | Fu Ning Du Chenglie Li Jianliang Liu Zhiqiang Peng Han |
| Abstract: | |
| Keywords: | complex embedded real-time system architecture analysis and design language (AADL) UPPAAL schedulability analysis model checking |
| 本文献已被 万方数据 等数据库收录！ | |