A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems
This work addresses the challenge of ensuring real-time performance in distributed avionics systems, which is critical for safety in aerospace applications, but it appears incremental as it builds on existing model-checking techniques with a compositional twist.
The authors tackled the problem of schedulability analysis for Distributed Integrated Modular Avionics (DIMA) systems, which are large and complex, by developing a compositional approach using model checking with stopwatch automata in UPPAAL, and they applied it to a concrete system to verify task deadlines and communication constraints.
This work presents a compositional approach for schedulability analysis of Distributed Integrated Modular Avionics (DIMA) systems that consist of spatially distributed ARINC-653 modules connected by a unified AFDX network. We model a DIMA system as a set of stopwatch automata in UPPAAL to verify its schedulability by model checking. However, direct model checking is infeasible due to the large state space. Therefore, we introduce the compositional analysis that checks each partition including its communication environment individually. Based on a notion of message interfaces, a number of message sender automata are built to model the environment for a partition. We define a timed selection simulation relation, which supports the construction of composite message interfaces. By using assume-guarantee reasoning, we ensure that each task meets the deadline and that communication constraints are also fulfilled globally. The approach is applied to the analysis of a concrete DIMA system.