Binary Code Level Verification for Interrupt Safety Properties of Real-Time Operating System

Interrupt mechanism is indispensable in embedded software due to lots of factors such as switching context and enhancing efficiency. In this context, the traditional way to ensure the correctness of software will not remain in force. Having the interrupt is envolved, the complicated and nondeterminism environment should be taken into consideration during the verification process. In this paper, we propose a novel way to verify the interrupt safety properties based on low-level binary code. At first, an Abstract xBIL is transformed from the xBIL with the time and interrupt properties reserved. xBIL [1] is a binary intermediate language we proposed to represent the machine instructions on multiple architectures. Afterwards, we present an automatic way to construct the Discrete-Time Markov Chains [2] from the Abstract xBIL code. After that, the properties can be easily generated and quantitative analysis could be performed. To prove the feasibility of our approach, we have applied our method to the verification of a commercial automotive operating system and it is proved to be of great help with the development of software.