Verifying OSEK/VDX automotive applications: A Spin‐based model checking approach. (19th February 2018)

• Record Type: Journal Article
• Authors: Zhang, Haitao; Li, Guoqiang; Cheng, Zhuo; Xue, Jinyun
• Is Part Of: Software testing, verification & reliability. Volume 28:Number 3(2018)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2018-02-19
• Subjects: deterministic scheduler -- interruption -- model checking -- OSEK/VDX -- Spin; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1662
• Languages: English
• ISSNs: 0960-0833

Abstract

Summary: OSEK/VDX, a development standard for automobiles, has now been widely adopted by automotive manufacturers for developing a vehicle‐mounted system. The ever increasing complexity of the system has created a challenge for ensuring the reliability of the developed OSEK/VDX applications in exhaustive way. Model checking as an exhaustive verification technique has attracted much attention in the automotive industry. To check OSEK/VDX applications by using model checking verification techniques, we have proposed a method based on SMT‐based bounded model checking. However, the method performs a poor efficiency in checking the OSEK/VDX applications that hold many loops, especially it is unable to deal with interruptions. In this paper, to apply model checking verification techniques to check a practical OSEK/VDX application, we develop and investigate an alterative approach based on the well‐known model checker Spin. In our Spin‐based approach, interruptions are taken into account, and moreover, 2 optimization strategies are used to boost the scalability and efficiency of the approach by reducing state space and accelerating bug detection. We have investigated the Spin‐based approach based on a series of experiments. The experimental results show that the approach is an impactful technique to verify the developed OSEK/VDX applications that hold a number of loops and interruptions. Abstract : OSEK/VDX application is a deterministic scheduler‐based multitasking software for vehicle‐mounted system. How to exhaustively check such application has become a challenge in automotive industry. This paper shows a method to solve this problem based on the model checker Spin.