Conformance Testing for OSEK/VDX Operating System Using Model Checking

Automotive systems are being standardized by several organizations because they use many parts developed by various companies. Thus, ensuring that those parts conform to standards is very important in this field. Moreover, the automotive systems require high reliability since their bugs or errors may cause serious accidents. In this paper, we focus on operating systems compliant with an OSEK/VDX standard, and propose a method to obtain highly reliable test cases for ensuring the conformance. So far, we have developed a design model based on the standard and made great effort to check that it conforms to the standard with a model checking tool SPIN. Our idea is to use this design model as a test oracle to automatically generate exhaustive test cases with the help of the model checking tool.