ZHANG, Min's webpage
An executable formal semantics of OSEK/VDX
Background
The OSEK/VDX standard is a generic description which is mandatory for any implementation of an OSEK/VDX operating system. It concerns the general description of the strategy and functionality, standardized application program- ming interface (API), resource management, event mechanism, etc.
K is a rewrite-based executable semantics framework developed at UIUC. Programming languages, calculi, as well as type systems or formal analysis tools can be defined in K.
Foraml semantics
We define a formal semantics ( see the definition here ) of OSEK/VDX in K. With the formal semantics, we can verify OSEK/VDX-based applications by symbolically executing them in K, and generate test cases automatically for given configuration of applications.
We show how to find deadlock state of a simplified tire pressure monitor application. By executing the application in K, we found a state where task RT tries to activate task ST which is at the waiting state.
Related paper
M. Zhang, Yunja Choi, K. Ogata
A Formal Semantics of the OSEK/VDX Standard in K Framework and its Applications
10th WRLA, LNCS, Grenoble, France, 2014. [pdf]
Admin. zhangmin@jaist.ac.jp
Ogata Laboratory
Last modified. 2013/06/15