Paper Info
Title
Binary Code Level Verification for Interrupt Safety Properties of Real-Time Operating System
Abstract
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.
Year
DOI
Venue
2012
10.1109/TASE.2012.46
TASE
Keywords
Field
DocType
complicated unstable environment,real-time operating system,discrete-time markov chains,binary intermediate language,interrupt safety properties,interrupt property,abstract xbil code,interrupt mechanism,low-level binary code,abstract xbil,embedded software,commercial automotive operating system,binary code level verification,operating systems,software development,real time systems,quantitative analysis,probabilistic logic,realtime operating system,embedded systems,interrupt,markov processes,rtos,software engineering,binary codes,binary code
Interrupt,Markov process,Embedded software,Computer science,Correctness,Binary code,Real-time operating system,Real-time computing,Software,Embedded system,Software verification
Conference
Citations 
PageRank 
References 
1
0.39
4
Authors
7
Name
Order
Citations
PageRank
Jianqi Shi15712.50
Longfei Zhu2356.10
Yanhong Huang34910.56
Jian Guo494.61
Huibiao Zhu558386.68
Huixing Fang6124.71
Xin Ye7266.44