Projects per year
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.
Original language | English |
---|---|
Title of host publication | Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation |
Editors | John P. Gallagher, Rob van Glabbeek, Wendelin Serwe |
Number of pages | 19 |
Volume | 268 |
Publisher | EPTCS |
Publication date | 27 Mar 2018 |
Pages | 150-168 |
DOIs | |
Publication status | Published - 27 Mar 2018 |
Event | 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018 - Thessaloniki, Greece Duration: 20 Apr 2018 → … |
Conference
Conference | 3rd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, MARSVPT 2018 |
---|---|
Country/Territory | Greece |
City | Thessaloniki |
Period | 20/04/2018 → … |
Series | Electronic Proceedings in Theoretical Computer Science |
---|---|
ISSN | 2075-2180 |
Fingerprint
Dive into the research topics of 'A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Compositional Verification of Real-time MULTI-CORE SAFETY Critical Systems
Nyman, U. (PI), Nielsen, B. (Other), Thi Xuan Phan, L. (Project Participant), Lee, I. (Project Participant), Legay, A. B. E. (Project Participant), Boudjadar, J. (Contact) & Kim, J. H. (Contact)
Independent Research Fund Denmark | Technology and Production sciences
01/08/2017 → 31/07/2021
Project: Other
-
Schedulability Analysis of Distributed Multi-core Avionics Systems with UPPAAL
Han, P., Zhai, Z., Nielsen, B., Nyman, U. & Kristjansen, M., 1 Nov 2019, In: Journal of Aerospace Information Systems. 16, 11Research output: Contribution to journal › Journal article › Research › peer-review
Open AccessFile6 Citations (Scopus)247 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. (eds.). p. 39-51 13 p. (Electronic Proceedings in Theoretical Computer Science, Vol. 272).Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review
Open AccessFile6 Citations (Scopus)133 Downloads (Pure)