ISSN 1000-1239 CN 11-1777/TP

Journal of Computer Research and Development ›› 2015, Vol. 52 ›› Issue (1): 167-176.doi: 10.7544/issn1000-1239.2015.20130722

Previous Articles     Next Articles

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

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

CLC Number: