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

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

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review


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 languageEnglish
Title of host publication2022 25th Euromicro Conference on Digital System Design (DSD)
EditorsHimar Fabelo, Samuel Ortega, Amund Skavhaug
PublisherInstitute of Electrical and Electronics Engineers
Pages 679-688
Number of pages10
ISBN (Electronic)978-1-6654-7404-7
Publication statusPublished - Sept 2022
Event25th Euromicro Conference on Digital System Design: DSD 2022 - ExpoMeloneras, Maspalomas, Spain
Duration: 31 Aug 20222 Sept 2022
Conference number: 25


Conference25th Euromicro Conference on Digital System Design
Abbreviated titleDSD 2022
Internet address


  • 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


Dive into the research topics of 'Verifying Liveness and Real-Time of OS-Based Embedded Software'. Together they form a unique fingerprint.

Cite this