TY - GEN
T1 - Modeling and verifying the code-level OSEK/VDX operating system with CSP
AU - Huang, Yanhong
AU - Zhao, Yongxin
AU - Zhu, Longfei
AU - Li, Qin
AU - Zhu, Huibiao
AU - Shi, Jianqi
PY - 2011
Y1 - 2011
N2 - As an automotive industry standard of operating system specification, OSEK/VDX is widely applied in the process of designing and implementing the static operating system and the corresponding interfaces for automotive electronics. It is challenging to explore an effective method to support large-scale correctness verification of OSEK/VDX specification. In this paper, we employ process algebra CSP to describe and reason about a real code-level OSEK/VDX operating system. Thus the whole system is formally modeled as a CSP process which is encoded and implemented in process analysis toolkit (PAT). Furthermore, the expected properties are described and expressed in terms of the first-order logic. The properties are also established and verified in our framework. The result indicates that the whole system is deadlock-free and the scheduling scheme is sound with respect to the specification.
AB - As an automotive industry standard of operating system specification, OSEK/VDX is widely applied in the process of designing and implementing the static operating system and the corresponding interfaces for automotive electronics. It is challenging to explore an effective method to support large-scale correctness verification of OSEK/VDX specification. In this paper, we employ process algebra CSP to describe and reason about a real code-level OSEK/VDX operating system. Thus the whole system is formally modeled as a CSP process which is encoded and implemented in process analysis toolkit (PAT). Furthermore, the expected properties are described and expressed in terms of the first-order logic. The properties are also established and verified in our framework. The result indicates that the whole system is deadlock-free and the scheduling scheme is sound with respect to the specification.
UR - https://www.scopus.com/pages/publications/80055116171
U2 - 10.1109/TASE.2011.11
DO - 10.1109/TASE.2011.11
M3 - 会议稿件
AN - SCOPUS:80055116171
SN - 9780769545066
T3 - Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
SP - 142
EP - 149
BT - Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
T2 - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
Y2 - 29 August 2011 through 31 August 2011
ER -