The embedded software development process employs various methodologies to support long term maintenance, portability and correctness. In general, the code based implementations involve configuration based approaches to improve maintenance. They are validated through rigorous testing strategies but hidden mode of failures are possible. Recently, Model Based Development (MBD) approaches are used to model the system and verify or validate the correctness against the requirements. This reduces the need for hardware based validation strategies and supports portability.

One such approach is the use of formal methods to model and verify the correctness of the system. Conventionally, the modeling of hardware independent implementations are achieved to a greater extent, but it is a prevalent challenge to model and verify the low-level implementations such as assembly code sequences. Modeling and verifying the low-level code implementation demands hardware architecture to be modeled. This increases complexity and could induce state space explosion.

With an objective to address these problems, the proposed method is to employ an abstract interpretation based static WCET analysis tool OTAWA, with the formal model tool Uppaal. The approach is to perform static analysis of cache, pipeline, etc., on the generated low-level code using the OTAWA framework. The results of these analyses (WCET timing, execution information, etc.) are then validated and used to create formal models of low-level code in Uppaal as timed automata. These models are composed and verified for safety, liveness, and reliability using Timed Computational Tree Logic (TCTL) formulas. The context switch sequences of a classic AUTOSAR OS for the Tricore TC275T architecture and SmartOS for a RISC-V architecture are taken as proofs of concept for the proposed methodology.