A Spin-Based Approach for Checking OSEK/VDX Applications

OSEK/VDX, a standard of automobile OS, has been widely adopted by many manufacturers to design and develop a vehicle-mounted OS. With the increasing functionalities in vehicles, more and more applications are developed based on the OSEK/VDX OS. However, how to ensure the reliability of the developed OSEK/VDX applications is becoming a challenge for developers. As to ensure the reliability of the developed OSEK/VDX applications, model checking as an exhaustive checking technique can be applied to verify the developed OSEK/VDX applications. In our previous work, we have proposed a bounded model checking approach to verify the OSEK/VDX applications. In this paper, we describe and develop an alternative approach to verify the OSEK/VDX applications based on the Spin. There are two motivations in this paper, one is to show how to use Spin to verify the OSEK/VDX applications, and the other is to investigate the effectiveness of our bounded model checking approach and Spin-based approach based on the experiments.