Modern embedded software development uses model-based methods to support long-term maintenance, portability, and correctness. A growing trend is to use formal methods to create software models and verify their correctness against requirement specifications. However, modeling and verifying low-level Real-Time Operating Systems (RTOS) or Basic Software (BSW) code sequences remains a major challenge, as it requires correctness against the internal hardware behavior and timing. To ensure this correctness, we need formal models of the complex hardware architecture, and due to the increased model complexity, the verification can lead to a state space explosion. In this paper, we mitigate these challenges by using an existing static Worst-Case Execution Time (WCET) analysis tool, OTAWA, for microarchitecture analysis. We use the intermediate results of the WCET analysis as input to our process, which verifies the correctness of the low-level implementations against the runtime effects of the hardware (e.g., synchronization dependencies, memory race conditions) and analyzes the timing and performance of the low-level code with respect to the data hazards in the pipeline. After successful verification, the results can be used in a formal method environment to model and verify the low-level code for correctness against the timing and requirement specifications. We demonstrate the proposed framework by analyzing and verifying the low-level context switch sequence of a classic AUTOSAR-based RTOS and the kernel startup sequence of FreeRTOS for correctness against hardware effects in the AURIX TriCore architecture. In addition, we show an empirical evaluation of our framework to examine the scalability, performance, and state space.
