ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2015, Vol. 52 ›› Issue (1): 167-176.doi: 10.7544/issn1000-1239.2015.20130722

• 软件技术 • 上一篇    下一篇

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

符宁1,杜承烈1,李建良2,刘志强3,彭寒4   

  1. 1(西北工业大学计算机学院 西安 710072); 2(西北农林科技大学信息工程学院 陕西杨凌 712100); 3(西北工业大学软件学院 西安 710072); 4(西安航空学院计算机工程系 西安 710077) (funingg@163.com)
  • 出版日期: 2015-01-01
  • 基金资助: 
    基金项目：国家“八六三”高技术研究发展计划基金项目(2011AA010102)|中国航空科学基金项目(20115553023)

Analysis and Verification of AADL Hierarchical Schedulers

Fu Ning1,Du Chenglie1,Li Jianliang2,Liu Zhiqiang3,Peng Han4   

  1. 1(School of Computer Science, Northwestern Polytechnical University, Xi’an 710072); 2(College of Information Engineering, Northwest A&F University, Yangling, Shaanxi 712100); 3(School of Software and Microelectronics, Northwestern Polytechnical University, Xi’an 710072); 4(School of Computer Engineering, Xi’an Aeronautical University, Xi’an 710077)
  • Online: 2015-01-01

RichHTML

1

PDF

665

被引次数

8

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

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

Abstract: In the system based on a hierarchical scheduler, the processor is shared between several collaborative schedulers. Such schedulers are becoming more and more investigated and proposed in reallife applications. For example, the ARINC 653 international standard which defines programming interface for avionic real time operating systems provides such a kind of collaborative schedulers. This article focuses on the modeling and the schedulability analysis of hierarchical schedulers. We investigate the modeling of hierarchical schedulers with architecture analysis and design language (AADL). A model checking based method for analyzing the schedulability of AADL hierarchical schedulers is proposed. The AADL thread components and hierarchical schedulers are modeled as network of timed automatons. The schedulability is described as a set of temporal logic formulas. Then we use a model checker Uppaal to analyze and verify the schedulability of hierarchical schedulers. Our work shows that analyzing schedulability of AADL hierarchical schedulers by model checking is feasible. The method uses an exhaustive method to automate analyze the properties of a system by a model checker. Compared with related works, the proposed method produces more precise results.

Key words: complex embedded real-time system, architecture analysis and design language (AADL), UPPAAL, schedulability analysis, model checking

中图分类号: 

版权所有 © 《计算机研究与发展》编辑部
地址：北京2704信箱《计算机研究与发展》编辑部　邮编：100190
电话：（010）62620696；（010）62600350　 传真：（010）62620696　 Email：crad@ict.ac.cn
本系统由北京玛格泰克科技发展有限公司设计开发　技术支持：support@magtech.com.cn