A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems

Pujie Han, Zhengjun Zhai, Brian Nielsen, Ulrik Nyman

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

6 Citations (Scopus)
107 Downloads (Pure)

Abstract

This paper presents a modeling framework 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 (SWA) in UPPAAL to analyze its schedulability by classical model checking (MC) and statistical model checking (SMC). The framework has been designed to enable three types of analysis: global SMC, global MC, and compositional MC. This allows an effective methodology including (1) quick schedulability falsification using global SMC analysis, (2) direct schedulability proofs using global MC analysis in simple cases, and (3) strict schedulability proofs using compositional MC analysis for larger state space. The framework is applied to the analysis of a concrete DIMA system.
Original languageEnglish
Title of host publicationProceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation
EditorsJohn P. Gallagher, Rob van Glabbeek, Wendelin Serwe
Number of pages19
Volume268
PublisherEPTCS
Publication date27 Mar 2018
Pages150-168
DOIs
Publication statusPublished - 27 Mar 2018
Event3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018 - Thessaloniki, Greece
Duration: 20 Apr 2018 → …

Conference

Conference3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018
CountryGreece
CityThessaloniki
Period20/04/2018 → …
SeriesElectronic Proceedings in Theoretical Computer Science
ISSN2075-2180

Fingerprint Dive into the research topics of 'A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems'. Together they form a unique fingerprint.

Cite this