A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems

TL;DR

This paper introduces a compositional model checking approach for schedulability analysis of distributed avionics systems, enabling scalable verification of complex ARINC-653 modules connected via AFDX networks.

Contribution

It proposes a novel compositional analysis method using message interfaces and assume-guarantee reasoning to verify schedulability of distributed avionics systems efficiently.

Findings

Successfully applied to a real DIMA system

Reduces state space complexity in model checking

Ensures global communication and timing constraints

Abstract

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.