An executable formal semantics of OSEK/VDX
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.
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.