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 proceedingKonferenceartikel i proceedingForskningpeer review

1 Citation (Scopus)
47 Downloads (Pure)

Resumé

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.
OriginalsprogEngelsk
TitelProceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design
RedaktørerSimon Bliudze, Saddek Bensalem
Antal sider13
Publikationsdato26 jun. 2018
Sider39-51
DOI
StatusUdgivet - 26 jun. 2018
BegivenhedInternational Workshop on Methods and Tools for Rigorous System Design - Thessaloniki, Grækenland
Varighed: 15 apr. 201815 apr. 2018
Konferencens nummer: 1
https://project.inria.fr/metrid2018/

Workshop

WorkshopInternational Workshop on Methods and Tools for Rigorous System Design
Nummer1
LandGrækenland
ByThessaloniki
Periode15/04/201815/04/2018
Internetadresse
NavnElectronic Proceedings in Theoretical Computer Science
Vol/bind272
ISSN2075-2180

Citer dette

Han, P., Zhai, Z., Nielsen, B., & Nyman, U. M. (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 (s. 39-51). Electronic Proceedings in Theoretical Computer Science, Bind. 272 https://doi.org/10.4204/EPTCS.272.4
Han, Pujie ; Zhai, Zhengjun ; Nielsen, Brian ; Nyman, Ulrik Mathias. / A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems. 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).
@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 = "6",
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",

}

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; Nyman, Ulrik Mathias.

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 proceedingKonferenceartikel i proceedingForskningpeer 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

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

ER -

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