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. In the verification, the complicated unstable environment after the interrupt is involved should be considered. In this paper, we propose a novel way to verify the interrupt 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 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 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.