Compositional Schedulability Analysis of An Avionics System Using UPPAAL

Abstract—We propose a compositional framework for analyz-ing the schedulability of hierarchical scheduling systems. The framework is realized using Parameterized Stopwatch Automata to describe tasks, whereas the schedulability analysis is per-formed using UPPAAL. The concrete behavior of each periodic preemptive task is given as a list of timed actions to which resources are assigned by SIRAP protocol. Our framework is reconfigurable in which the hierarchical structure, the scheduling policies, the concrete task behavior and the shared resources can all be reconfigured. Finally, we use our framework to analyze the schedulability of a real-time avionics system. Keywords-Hierarchical scheduling systems, Parameterized stopwatch automata, Compositional analysis, Uppaal