A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems

Pujie Han, Zhengjun Zhai, Brian Nielsen, Ulrik Mathias Nyman

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

5 Citations (Scopus)
78 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design
EditorsSimon Bliudze, Saddek Bensalem
Number of pages13
Publication date26 Jun 2018
Pages39-51
DOIs
Publication statusPublished - 26 Jun 2018
EventInternational Workshop on Methods and Tools for Rigorous System Design - Thessaloniki, Greece
Duration: 15 Apr 201815 Apr 2018
Conference number: 1
https://project.inria.fr/metrid2018/

Workshop

WorkshopInternational Workshop on Methods and Tools for Rigorous System Design
Number1
CountryGreece
CityThessaloniki
Period15/04/201815/04/2018
Internet address
SeriesElectronic Proceedings in Theoretical Computer Science
Volume272
ISSN2075-2180

Cite this