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

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.