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

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

6 Citationer (Scopus)

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

Originalsprog	Engelsk
Titel	Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design
Redaktører	Simon Bliudze, Saddek Bensalem
Antal sider	13
Publikationsdato	26 jun. 2018
Sider	39-51
DOI	https://doi.org/10.4204/EPTCS.272.4
Status	Udgivet - 26 jun. 2018
Begivenhed	International Workshop on Methods and Tools for Rigorous System Design - Thessaloniki, Grækenland Varighed: 15 apr. 2018 → 15 apr. 2018 Konferencens nummer: 1 https://project.inria.fr/metrid2018/

Workshop

Workshop	International Workshop on Methods and Tools for Rigorous System Design
Nummer	1
Land/Område	Grækenland
By	Thessaloniki
Periode	15/04/2018 → 15/04/2018
Internetadresse	https://project.inria.fr/metrid2018/

Navn	Electronic Proceedings in Theoretical Computer Science
Vol/bind	272
ISSN	2075-2180

Adgang til dokumentet

10.4204/EPTCS.272.4Licens: CC BY 3.0

MeTRiD2018.4Forlagets udgivne version, 338 KBLicens: CC BY 3.0

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

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Andre filer og links

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

1 Afsluttet

Compositional Verification of Real-time MULTI-CORE SAFETY Critical Systems
Nyman, U., Nielsen, B., Thi Xuan Phan, L., Lee, I., Legay, A. B. E., Boudjadar, J. & Kim, J. H.
Danmarks Frie Forskningsfond | Teknologi og Produktion
01/08/2017 → 31/07/2021
Projekter: Projekt › Andet

6 Citationer
1 Konferenceartikel i proceeding
1 Tidsskriftartikel

Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL
Han, P., Zhai, Z., Nielsen, B., Nyman, U. & Kristjansen, M., 1 nov. 2019, I: Journal of Aerospace Information Systems. 16, 11
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › peer review

Åben adgang
Fil
4 Citationer (Scopus)

176 Downloads (Pure)
A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems
Han, P., Zhai, Z., Nielsen, B. & Nyman, U., 27 mar. 2018, Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Gallagher, J. P., van Glabbeek, R. & Serwe, W. (red.). EPTCS, Bind 268. s. 150-168 19 s. (Electronic Proceedings in Theoretical Computer Science).
Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

Åben adgang
Fil
6 Citationer (Scopus)

169 Downloads (Pure)

Citationsformater

@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. i S Bliudze & S Bensalem (red), Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design. Electronic Proceedings in Theoretical Computer Science, bind 272, s. 39-51, International Workshop on Methods and Tools for Rigorous System Design, Thessaloniki, Grækenland, 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. red. / Simon Bliudze; Saddek Bensalem. 2018. s. 39-51 (Electronic Proceedings in Theoretical Computer Science, Bind 272).

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › 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

Adgang til dokumentet

AUB Link

Andre filer og links

Projekter

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

Publikation

Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL

A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems

Citationsformater