Analysis and verification of AADL hierarchical schedulers

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.