Projects per year
Abstract
Porting software to new target architectures is a common challenge, particularly when dealing with low-level functionality in drivers or OS kernels that interact directly with hardware. Traditionally, adapting code for different hardware platforms has been a manual and error-prone process. However, with the growing demand for dependability and the increasing hardware diversity in systems like the IoT, new software development approaches are essential. This includes rigorous methods for verifying and automatically porting Real-Time Operating Systems (RTOS) to various devices. Our framework addresses this challenge through formal methods and code generation for embedded RTOS. We demonstrate a hardware-specific part of a kernel model in Event-B, ensuring correctness according to the specification. Since hardware details are only added in late modeling stages, we can reuse most of the model and proofs for multiple targets. In a proof of concept, we refine the generic model for two different architectures, also ensuring safety and liveness properties. We then showcase automatic low-level code generation from the model. Finally, a hardware-independent factorial function model illustrates more potential of our approach.
Original language | English |
---|---|
Pages (from-to) | 289-315 |
Number of pages | 27 |
Journal | Software and Systems Modeling |
Volume | 23 |
Issue number | 2 |
Early online date | 1 Feb 2024 |
DOIs | |
Publication status | Published - Apr 2024 |
Keywords
- Code generation
- Embedded systems
- Event-B
- Formal methods
- Portability
- RTOS
- Verification
ASJC Scopus subject areas
- Software
- Modelling and Simulation
Fields of Expertise
- Information, Communication & Computing
Projects
- 3 Finished
-
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
-
Reconfigurable Processor Architectures
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)) & Saikia, A. (Co-Investigator (CoI))
1/09/14 → 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