A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems

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

doi:10.4204/EPTCS.272.4

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 proceeding › Article in proceeding › Research › peer-review

6 Citations (Scopus)

129 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 language	English
Title of host publication	Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design
Editors	Simon Bliudze, Saddek Bensalem
Number of pages	13
Publication date	26 Jun 2018
Pages	39-51
DOIs	https://doi.org/10.4204/EPTCS.272.4
Publication status	Published - 26 Jun 2018
Event	International Workshop on Methods and Tools for Rigorous System Design - Thessaloniki, Greece Duration: 15 Apr 2018 → 15 Apr 2018 Conference number: 1 https://project.inria.fr/metrid2018/

Workshop

Workshop	International Workshop on Methods and Tools for Rigorous System Design
Number	1
Country/Territory	Greece
City	Thessaloniki
Period	15/04/2018 → 15/04/2018
Internet address	https://project.inria.fr/metrid2018/

Series	Electronic Proceedings in Theoretical Computer Science
Volume	272
ISSN	2075-2180

Access to Document

10.4204/EPTCS.272.4Licence: CC BY 3.0

MeTRiD2018.4Final published version, 338 KBLicence: CC BY 3.0

http://eptcs.web.cse.unsw.edu.au/paper.cgi?MeTRiD2018.4.pdf

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@inproceedings{1b7e307d46aa443eb0660a9db24700c5,

title = "A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems",

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.",

author = "Pujie Han and Zhengjun Zhai and Brian Nielsen and Nyman, {Ulrik Mathias}",

year = "2018",

month = jun,

day = "26",

doi = "10.4204/EPTCS.272.4",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "Open Publishing Association",

pages = "39--51",

editor = "Simon Bliudze and Saddek Bensalem",

booktitle = "Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design",

note = "International Workshop on Methods and Tools for Rigorous System Design ; Conference date: 15-04-2018 Through 15-04-2018",

url = "https://project.inria.fr/metrid2018/",

}

Han, P, Zhai, Z, Nielsen, B & Nyman, UM 2018, A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems. in S Bliudze & S Bensalem (eds), Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design. Electronic Proceedings in Theoretical Computer Science, vol. 272, pp. 39-51, International Workshop on Methods and Tools for Rigorous System Design, Thessaloniki, Greece, 15/04/2018. https://doi.org/10.4204/EPTCS.272.4

A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems. / Han, Pujie; Zhai, Zhengjun; Nielsen, Brian et al.
Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design. ed. / Simon Bliudze; Saddek Bensalem. 2018. p. 39-51 (Electronic Proceedings in Theoretical Computer Science, Vol. 272).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

T1 - A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems

AU - Han, Pujie

AU - Zhai, Zhengjun

AU - Nielsen, Brian

AU - Nyman, Ulrik Mathias

N1 - Conference code: 1

PY - 2018/6/26

Y1 - 2018/6/26

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85056251914&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.272.4

DO - 10.4204/EPTCS.272.4

M3 - Article in proceeding

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 39

EP - 51

BT - Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design

A2 - Bliudze, Simon

A2 - Bensalem, Saddek

T2 - International Workshop on Methods and Tools for Rigorous System Design

Y2 - 15 April 2018 through 15 April 2018

ER -

A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems

Abstract

Workshop

Access to Document

AUB Link

Other files and links

Compositional Verification of Real-time MULTI-CORE SAFETY Critical Systems

Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL

A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems

Cite this

A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems

Abstract

Workshop

Access to Document

AUB Link

Other files and links

Projects

Compositional Verification of Real-time MULTI-CORE SAFETY Critical Systems

Research output

Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL

A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems

Cite this