Modelling and Verification of ARINC 653 Hierarchical Preemptive Scheduling
Ning Fu, Lijun Shan,
Chenglie Du, Zhiqiang Liu, and Han Peng
School of Computer Science, Northwestern
Polytechnical University, China
Abstract: 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.
Keywords: ARINC653, schedulability
analysis, model checking, UPPAAL.
Received June 15, 2016; accepted March 19,
2019
https://doi.org/10.34028/iajit/17/1/12