Formal model-based conformance verification of an OSEK/VDX compliant RTOS

The conformance of a real time operating system (RTOS) to the OSEK/VDX standard is usually achieved by doing tests where a set of test cases is performed on the RTOS. However, in an embedded system, it is often necessary to specialize (configure) the code of the RTOS according to the requirements of the application. For such specialized RTOS, some conformance test cases can not be applied because they need some functionalities that are not supported anymore. This paper presents a model-based conformance verification of a RTOS with the OSEK/VDX standard. The method is applied on Trampoline RTOS which is used both for industry and academic purposes and which have been entirely and formally modeled by a product of extended finite automata embedding its source code. The first step is the construction of a complete model that describes the interaction between the application and the RTOS. In the second step all OSEK/VDX conformance test cases are translated into observers and composed with the complete model. Then, for a particular application, The observers allow to check if the RTOS model meets the OSEK/VDX specification. The interest of our approach is twofold: i) it allows to check the OSEK/VDX conformance of the complete version of the Trampoline RTOS; ii) for a specialized version of the RTOS, it identifies the relevant test cases for the given application, that require a very carefully conformance testing.