Projects per year
Abstract
Embedded devices are fundamental to a huge variety of application areas, with a wide range of complexity and criticality. Therefore, they must satisfy a variety of (non-)functional requirements, and reliable strategies are necessary to guarantee that these requirements are met. As an additional complication, modern software systems are composed from various modules that interact and interfere at runtime. Operating Systems (OSes) are then used to manage the concurrency, but introduce additional complexity and runtime effects. Where testing is no longer sufficient to assess the software correctness, formal methods are becoming increasingly popular. Respecting the typical layering in embedded software, we propose a generic formal modeling scheme for OS-based application tasks and the formal verification of their liveness and real-time requirements. We use UPPAAL to model the software composition as the conjunction of application tasks and the OS, and for taking the interaction and interference of tasks through the OS into account. Despite of focusing on only two requirements in this paper, the modeling strategy is generic and extensible, meaning that additional requirements can be modeled and verified in a similar manner. An evaluation shows the general benefit of the approach as well as the impact of various factors on the verification complexity and scalability.
Original language | English |
---|---|
Title of host publication | 2022 25th Euromicro Conference on Digital System Design (DSD) |
Editors | Himar Fabelo, Samuel Ortega, Amund Skavhaug |
Publisher | IEEE |
Pages | 679-688 |
Number of pages | 10 |
ISBN (Electronic) | 978-1-6654-7404-7 |
DOIs | |
Publication status | Published - Sept 2022 |
Event | 25th Euromicro Conference on Digital System Design: DSD 2022 - ExpoMeloneras, Maspalomas, Spain Duration: 31 Aug 2022 → 2 Sept 2022 Conference number: 25 https://dsd-seaa2022.iuma.ulpgc.es/ |
Conference
Conference | 25th Euromicro Conference on Digital System Design |
---|---|
Abbreviated title | DSD 2022 |
Country/Territory | Spain |
City | Maspalomas |
Period | 31/08/22 → 2/09/22 |
Internet address |
Keywords
- Embedded Systems
- Formal Verification
- Real-Time Operating Systems
- Uppaal
ASJC Scopus subject areas
- Artificial Intelligence
- Information Systems
- Signal Processing
- Hardware and Architecture
Fields of Expertise
- Information, Communication & Computing
Fingerprint
Dive into the research topics of 'Verifying Liveness and Real-Time of OS-Based Embedded Software'. Together they form a unique fingerprint.-
CompEAS-BSW1 - Compositional Embedded Automotive Systems - Basic Software
Baunach, M. C. (Co-Investigator (CoI)), Manjunath, V. (Co-Investigator (CoI)), Nagarajan, D. (Co-Investigator (CoI)) & Krisper, M. (Co-Investigator (CoI))
1/11/20 → 31/03/25
Project: Research project
-
Embedded Operating Systems
Baunach, M. C. (Co-Investigator (CoI)), Martins Gomes, R. (Co-Investigator (CoI)), Batista Ribeiro, L. (Co-Investigator (CoI)), Malenko, M. (Co-Investigator (CoI)), Mauroner, F. (Co-Investigator (CoI)) & Scheipel, T. P. (Co-Investigator (CoI))
1/09/15 → 31/12/23
Project: Research project
-
Embedded Automotive Systems
Baunach, M. C. (Co-Investigator (CoI)), Batista Ribeiro, L. (Co-Investigator (CoI)), Martins Gomes, R. (Co-Investigator (CoI)), Malenko, M. (Co-Investigator (CoI)), Scheipel, T. P. (Co-Investigator (CoI)), Saikia, A. (Co-Investigator (CoI)), Nagarajan, D. (Co-Investigator (CoI)), Manjunath, V. (Co-Investigator (CoI)), Kissich, M. (Co-Investigator (CoI)) & Kanics, K. (Co-Investigator (CoI))
1/09/14 → 31/12/24
Project: Research area