An Approach for Checking OSEK/VDX Applications

With the growing demands for automotive auxiliary functions, more and more complex applications have been developed based on OSEK/VDX OS. However, how to completely check developed applications is becoming a challenge for developers. In this paper, we describe and develop an approach to check developed applications based on the SMT-based BMC. We have implemented a prototype tool and conducted some experiments. The experiments results show that our approach can be completely used to check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API and (iv) tasks execution sequences.