SMT-based bounded model checking for 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 check the developed applications is becoming a challenge for developers. Although some invaluable formal methods have been proposed to check actual software, these methods cannot be directly employed to check OSEK/VDX applications. In this paper, we describe and develop an approach to check OSEK/VDX applications using SMT-based bounded model checking. We also implement a prototype tool and conduct many experiments on several examples. The experiment results show that our approach can completely check the properties associated with (i) variables, (ii) mutual exclusion, (iii) service API, and (iv) tasks execution sequences of developed applications.