Verifying Liveness and Real-Time of OS-Based Embedded Software

Leandro Batista Ribeiro, Drona Nagarajan, Vignesh Manjunath, Muhammad Tanveer Ali Ahmad, Marcel Carsten Baunach

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandBegutachtung


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 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.
Titel25th Euromicro Conference on Digital System Design (DSD)
ErscheinungsortMaspalomas, Spain
Herausgeber (Verlag)EUROMICRO
PublikationsstatusAngenommen/In Druck - Sep. 2022
Veranstaltung25th Euromicro Conference on Digital System Design: DSD 2022 - ExpoMeloneras, Maspalomas, Spanien
Dauer: 31 Aug. 20222 Sep. 2022
Konferenznummer: 25


Konferenz25th Euromicro Conference on Digital System Design
KurztitelDSD 2022

Fields of Expertise

  • Information, Communication & Computing


Untersuchen Sie die Forschungsthemen von „Verifying Liveness and Real-Time of OS-Based Embedded Software“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren