liu.seSearch for publications in DiVA
Planned maintenance
A system upgrade is planned for 24/9-2024, at 12:00-14:00. During this time DiVA will be unavailable.
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Abstraction models for verifying resource adequacy of IMA systems at concept level
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0002-1485-0802
2021 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 208, article id 102654Article in journal (Refereed) Published
Abstract [en]

Complex cyber-physical systems can be difficult to analyze for resource adequacy (e.g., bandwidth and buffer size) at the concept development stage since relevant models are hard to create. During this period, details about the functions to be executed or the platforms in the architecture are partially unknown. This is especially true for Integrated Modular Avionics (IMA) systems, for which life-cycles span over several decades, with potential changes to functionality in the future. This work aims to identify abstractions for representing data exchanges among functions realized in networked IMA systems and investigates how these can be represented in formal models and analyzed with exact guarantees. Timed automata (TA) are a relevant choice for modeling since communication resource adequacy is directly related to potential network delays. We explore two alternatives in modeling with TA, a direct one representing every process using a TA template, and a more abstract one representing every computation device with a TA template. While the first approach represents process-to-process data exchanges, the modified approach reduces the state space by representing all processes currently allocated to a single computing element to obtain scalability gains. Both approaches are flexible since the templates presented can be instantiated to represent different types of network topologies and communication patterns. The instantiated TA models are used to illustrate an use case and analyzed with the UPPAAL model checker to verify that a given platform instance supports the desired system functions in terms of network bandwidth and buffer size adequacy, thereby messages reaching their final destination with freshness guarantees. Both abstraction levels are shown to be suitable for verifying the intended properties, but the more abstract one demonstrates a 67% improvement in verification time and a 66% reduction in state space during verification. The more abstract approach is also applied to a real-world example from an earlier publication, with a much larger state space and a more complex structure, to illustrate the ability to reuse the approach in multiple use cases. (C) 2021 The Authors. Published by Elsevier B.V.

Place, publisher, year, edition, pages
Elsevier , 2021. Vol. 208, article id 102654
Keywords [en]
IMA system; Conceptual analysis; Network resource adequacy; Timed automata; UPPAAL
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-176135DOI: 10.1016/j.scico.2021.102654ISI: 000652847700004OAI: oai:DiVA.org:liu-176135DiVA, id: diva2:1562026
Note

Funding Agencies|Swedish Governmental Agency for Innovation SystemsVinnova, as part of the national projects on aeronautics, NFFP7, project CLASSICS [NFFP7 201704890]

Available from: 2021-06-08 Created: 2021-06-08 Last updated: 2024-04-30
In thesis
1. Exploring Trade-offs in Concept Design of Integrated Modular Avionic Platform Configurations: Topology Generation, Resource Adequacy, and Dependability
Open this publication in new window or tab >>Exploring Trade-offs in Concept Design of Integrated Modular Avionic Platform Configurations: Topology Generation, Resource Adequacy, and Dependability
2024 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Modern aircraft heavily depend on computer systems to carry out various tasks. From managing flight surfaces and engines to processing radar and imagery data and facilitating communication with other aircraft and ground stations, computers are involved in almost every aspect of an aircraft’s operation. These computer systems, known as Integrated Modular Avionics (IMA) systems, have long life cycles that span several decades and undergo regular updates. Despite this, a significant portion of the overall life cycle costs is determined very early in the life cycle, in the concept design phase. 

While the early concept stage provides the best opportunity to influence the design of the system and its future costs, it is also the stage where information about the system is most limited. During this early stage, selecting a suitable IMA platform configuration must ensure sufficient resources for the intended aircraft functionalities, particularly in computing and networking capabilities. Additionally, the decisions regarding safety and security measures must align with application requirements. However, this is a complex task due to conflicting requirements, necessitating compromises, and the limited information available at this early stage. 

This thesis explores the analysis and generation of avionic architecture configurations during the concept stage, addressing the problem on two fronts. The first focuses on verifying whether a chosen IMA platform configuration provides sufficient resources to ensure timely communication for a specified set of avionic applications. The second centers on exploring the conceptual design space to find IMA platform configurations aligned with computing, networking, fault-tolerance, and security application needs. 

To contribute to the problem’s verification aspect, this thesis introduces two high-level abstractions, namely timed automata and a domain-specific model based on Unified Modelling Languages (UML), to model IMA systems at the concept stage. These are designed to capture inter-process message ex-changes within networked IMA platforms. Additionally, we propose a workflow and a supporting tool explicitly designed to translate our proposed model into a network calculus model for further analysis. The approach’s practicality and scalability are showcased through its application to an avionics use case. 

In exploring conceptual design space, this thesis proposes NetGAP, a domain-specific method in which interconnection patterns in generic networked system topologies are represented as graph grammars. Combined with Monte Carlo Tree Search and genetic algorithms, these grammars are used to navigate the solution space and generate candidate IMA platform configurations tailored to the requirements of an envisaged application. Through application to an avionics use case, NetGAP is shown to be scalable and suitable for different types of requirements. To further expedite the process, NetGAP has evolved into NeuralGAP. The latter employs graph neural networks to assess network topology compatibility with the target application, accelerating the concept exploration and improving its results.  

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press, 2024. p. 67
Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 2384
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-203166 (URN)10.3384/9789180756143 (DOI)9789180756136 (ISBN)9789180756143 (ISBN)
Public defence
2024-06-05, Key 1, Key-building, Campus Valla, Linköping, 13:00 (English)
Opponent
Supervisors
Funder
Vinnova, NFFP7 2017-04890; 2023-01183
Available from: 2024-04-30 Created: 2024-04-30 Last updated: 2024-05-24Bibliographically approved

Open Access in DiVA

fulltext(1850 kB)587 downloads
File information
File name FULLTEXT01.pdfFile size 1850 kBChecksum SHA-512
bf6536e7d89affed1d906cc94020ae9494423831a70e3622b0a49e5c74b4fa6ac07886854f9c0a2f015499094d17d40a374ff78052a8798a9570322bffc8c207
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Saar de Moraes, RodrigoNadjm-Tehrani, Simin
By organisation
Software and SystemsFaculty of Science & Engineering
In the same journal
Science of Computer Programming
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 587 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 647 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf