Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL

Pujie Han, Zhengjun Zhai, Brian Nielsen, Ulrik Nyman, Martin Kristjansen

Research output: Contribution to journalJournal articleResearchpeer-review

29 Downloads (Pure)

Abstract

This paper presents an approach for schedulability analysis of Distributed Integrated Modular Avionics (DIMA) systems that consist of spatially distributed ARINC-653 multicore modules connected by a unified Avionics Full-Duplex Switched Ethernet (AFDX) network. A multicore DIMA system is modeled as a set of stopwatch automata in uppaal to verify its schedulability by model checking. However, direct verification is infeasible due to the large state space. Therefore, global analysis based on statistical model checking (SMC) and compositional analysis based on classical model checking are combined, thereby mitigating the state space explosion problem. Even though the nature of SMC testing cannot prove schedulability, the model of a DIMA system first undergoes quick schedulability falsification using global SMC analysis. Thereafter, a compositional approach is used to check each partition, including its communication environment individually. By using assume-guarantee reasoning, it is ensured that each real-time task meets the deadline and that communication constraints are also fulfilled globally. The approach is finally applied to the schedulability analysis of a concrete multicore DIMA system.
Original languageEnglish
JournalJournal of Aerospace Information Systems
Volume16
Issue number11
ISSN2327-3097
DOIs
Publication statusPublished - 1 Nov 2019

Fingerprint

Avionics
Model checking
Stop watches
Communication
Ethernet
Explosions
Concretes
Testing
Statistical Models

Cite this

@article{cfa976bcb0f4438690673a9ec2dbfe52,
title = "Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL",
abstract = "This paper presents an approach for schedulability analysis of Distributed Integrated Modular Avionics (DIMA) systems that consist of spatially distributed ARINC-653 multicore modules connected by a unified Avionics Full-Duplex Switched Ethernet (AFDX) network. A multicore DIMA system is modeled as a set of stopwatch automata in uppaal to verify its schedulability by model checking. However, direct verification is infeasible due to the large state space. Therefore, global analysis based on statistical model checking (SMC) and compositional analysis based on classical model checking are combined, thereby mitigating the state space explosion problem. Even though the nature of SMC testing cannot prove schedulability, the model of a DIMA system first undergoes quick schedulability falsification using global SMC analysis. Thereafter, a compositional approach is used to check each partition, including its communication environment individually. By using assume-guarantee reasoning, it is ensured that each real-time task meets the deadline and that communication constraints are also fulfilled globally. The approach is finally applied to the schedulability analysis of a concrete multicore DIMA system.",
author = "Pujie Han and Zhengjun Zhai and Brian Nielsen and Ulrik Nyman and Martin Kristjansen",
year = "2019",
month = "11",
day = "1",
doi = "10.2514/1.I010715",
language = "English",
volume = "16",
journal = "Journal of Aerospace Information Systems",
issn = "2327-3097",
number = "11",

}

Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL. / Han, Pujie; Zhai, Zhengjun; Nielsen, Brian; Nyman, Ulrik; Kristjansen, Martin.

In: Journal of Aerospace Information Systems, Vol. 16, No. 11, 01.11.2019.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL

AU - Han, Pujie

AU - Zhai, Zhengjun

AU - Nielsen, Brian

AU - Nyman, Ulrik

AU - Kristjansen, Martin

PY - 2019/11/1

Y1 - 2019/11/1

N2 - This paper presents an approach for schedulability analysis of Distributed Integrated Modular Avionics (DIMA) systems that consist of spatially distributed ARINC-653 multicore modules connected by a unified Avionics Full-Duplex Switched Ethernet (AFDX) network. A multicore DIMA system is modeled as a set of stopwatch automata in uppaal to verify its schedulability by model checking. However, direct verification is infeasible due to the large state space. Therefore, global analysis based on statistical model checking (SMC) and compositional analysis based on classical model checking are combined, thereby mitigating the state space explosion problem. Even though the nature of SMC testing cannot prove schedulability, the model of a DIMA system first undergoes quick schedulability falsification using global SMC analysis. Thereafter, a compositional approach is used to check each partition, including its communication environment individually. By using assume-guarantee reasoning, it is ensured that each real-time task meets the deadline and that communication constraints are also fulfilled globally. The approach is finally applied to the schedulability analysis of a concrete multicore DIMA system.

AB - This paper presents an approach for schedulability analysis of Distributed Integrated Modular Avionics (DIMA) systems that consist of spatially distributed ARINC-653 multicore modules connected by a unified Avionics Full-Duplex Switched Ethernet (AFDX) network. A multicore DIMA system is modeled as a set of stopwatch automata in uppaal to verify its schedulability by model checking. However, direct verification is infeasible due to the large state space. Therefore, global analysis based on statistical model checking (SMC) and compositional analysis based on classical model checking are combined, thereby mitigating the state space explosion problem. Even though the nature of SMC testing cannot prove schedulability, the model of a DIMA system first undergoes quick schedulability falsification using global SMC analysis. Thereafter, a compositional approach is used to check each partition, including its communication environment individually. By using assume-guarantee reasoning, it is ensured that each real-time task meets the deadline and that communication constraints are also fulfilled globally. The approach is finally applied to the schedulability analysis of a concrete multicore DIMA system.

U2 - 10.2514/1.I010715

DO - 10.2514/1.I010715

M3 - Journal article

VL - 16

JO - Journal of Aerospace Information Systems

JF - Journal of Aerospace Information Systems

SN - 2327-3097

IS - 11

ER -