A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems

Pujie Han; Zhengjun Zhai; Brian Nielsen; Ulrik Nyman

doi:10.4204/EPTCS.268.5

A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems

Pujie Han, Zhengjun Zhai, Brian Nielsen, Ulrik Nyman

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

6 Citationer (Scopus)

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

Originalsprog	Engelsk
Titel	Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation
Redaktører	John P. Gallagher, Rob van Glabbeek, Wendelin Serwe
Antal sider	19
Vol/bind	268
Forlag	EPTCS
Publikationsdato	27 mar. 2018
Sider	150-168
DOI	https://doi.org/10.4204/EPTCS.268.5
Status	Udgivet - 27 mar. 2018
Begivenhed	3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018 - Thessaloniki, Grækenland Varighed: 20 apr. 2018 → …

Konference

Konference	3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018
Land/Område	Grækenland
By	Thessaloniki
Periode	20/04/2018 → …

Navn	Electronic Proceedings in Theoretical Computer Science
ISSN	2075-2180

Adgang til dokumentet

10.4204/EPTCS.268.5Licens: CC BY 3.0

A Modeling Framework for Schedulability Analysis of Distributed Avionics SystemsForlagets udgivne version, 1.000 KBLicens: CC BY 3.0

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Andre filer og links

Slides

1 Afsluttet

Compositional Verification of Real-time MULTI-CORE SAFETY Critical Systems
Nyman, U., Nielsen, B., Thi Xuan Phan, L., Lee, I., Legay, A., 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
2 Citationer (Scopus)

130 Downloads (Pure)
A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems
Han, P., Zhai, Z., Nielsen, B. & Nyman, U. M., 26 jun. 2018, Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design. Bliudze, S. & Bensalem, S. (red.). s. 39-51 13 s. (Electronic Proceedings in Theoretical Computer Science, Bind 272).
Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

Åben adgang
Fil

6 Citationer (Scopus)

116 Downloads (Pure)

Citationsformater

Han, P., Zhai, Z., Nielsen, B., & Nyman, U. (2018). A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems. I J. P. Gallagher, R. van Glabbeek, & W. Serwe (red.), Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation (Bind 268, s. 150-168). EPTCS. Electronic Proceedings in Theoretical Computer Science https://doi.org/10.4204/EPTCS.268.5

Han, Pujie ; Zhai, Zhengjun ; Nielsen, Brian et al. / A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems. Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. red. / John P. Gallagher ; Rob van Glabbeek ; Wendelin Serwe. Bind 268 EPTCS, 2018. s. 150-168 (Electronic Proceedings in Theoretical Computer Science).

@inproceedings{13b80ac8655a45918d135c9fccc61920,

title = "A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems",

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

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

year = "2018",

month = mar,

day = "27",

doi = "10.4204/EPTCS.268.5",

language = "English",

volume = "268",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "EPTCS",

pages = "150--168",

editor = "Gallagher, {John P.} and {van Glabbeek}, Rob and Wendelin Serwe",

booktitle = "Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation",

note = "3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018 ; Conference date: 20-04-2018",

}

Han, P, Zhai, Z, Nielsen, B & Nyman, U 2018, A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems. i JP Gallagher, R van Glabbeek & W Serwe (red), Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. bind 268, EPTCS, Electronic Proceedings in Theoretical Computer Science, s. 150-168, 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018, Thessaloniki, Grækenland, 20/04/2018. https://doi.org/10.4204/EPTCS.268.5

A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems. / Han, Pujie; Zhai, Zhengjun; Nielsen, Brian et al.
Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. red. / John P. Gallagher; Rob van Glabbeek; Wendelin Serwe. Bind 268 EPTCS, 2018. s. 150-168 (Electronic Proceedings in Theoretical Computer Science).

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

TY - GEN

T1 - A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems

AU - Han, Pujie

AU - Zhai, Zhengjun

AU - Nielsen, Brian

AU - Nyman, Ulrik

PY - 2018/3/27

Y1 - 2018/3/27

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

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

UR - http://mars-workshop.org/mars2018/MARSVPT2018.5.slides.pdf

U2 - 10.4204/EPTCS.268.5

DO - 10.4204/EPTCS.268.5

M3 - Article in proceeding

AN - SCOPUS:85048359714

VL - 268

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 150

EP - 168

BT - Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation

A2 - Gallagher, John P.

A2 - van Glabbeek, Rob

A2 - Serwe, Wendelin

PB - EPTCS

T2 - 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018

Y2 - 20 April 2018

ER -

Han P, Zhai Z, Nielsen B , Nyman U. A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems. I Gallagher JP, van Glabbeek R, Serwe W, red., Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Bind 268. EPTCS. 2018. s. 150-168. (Electronic Proceedings in Theoretical Computer Science). doi: 10.4204/EPTCS.268.5

A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems

Abstract

Konference

Adgang til dokumentet

AUB Link

Andre filer og links

Fingeraftryk

Projekter

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

Publikation

Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL

A Compositional Approach for Schedulability Analysis of Distributed Avionics Systems

Citationsformater