Modelling and Verification of ARINC 653 Hierarchical Preemptive Scheduling

Avionics Application Standard Software Interface (ARINC 653) is a software specification for space and time partitioning in safety-critical avionics real-time operating systems. Correctly designed task schedulers are crucial for ARINC 653 running systems. This paper proposes a model-checking-based method for analyzing and verifying ARINC 653 scheduling model. Based on priced timed automata theory, an ARINC 653 scheduling system was modelled as a priced timed automata network. The schedulability of the system was described as a set of temporal logic expressions, and was analyzed and verified by a model checker. Our research shows that it is feasible to use model checking to analyze task schedulability in an ARINC 653 hierarchical scheduling system. The method discussed modelled preemptive scheduling by using the stop/watch features of priced timed automata. Unlike traditional scheduling analysis techniques, the proposed approach uses an exhaustive method to automate analysis of the schedulability of a system, resulting in a more precise analysis.