Verifying OSEK/VDX automotive applications: A Spin‐based model checking approach
Verifying OSEK/VDX automotive applications: A Spin‐based model checking approach
复制标题
DOI：
10.1002/stvr.1662
复制
发表时间：
2018-02
期刊：
影响因子：
--
通讯作者：
Haitao Zhang;Guoqiang Li;Zhuo Cheng;Jinyun Xue
中科院分区：
文献类型：
--
作者：
Haitao Zhang;Guoqiang Li;Zhuo Cheng;Jinyun Xue
OSEK/VDX是一项汽车开发标准，现已被汽车制造商广泛采用，用于开发车载系统。系统的复杂性不断增加，为确保开发的OSEK/VDX应用程序的全面可靠性带来了挑战。模型检验作为一种彻底的验证技术，在汽车工业中受到了广泛的关注。为了使用模型检查验证技术来检查OSEK/VDX应用程序，我们提出了一种基于SMT的有界模型检查方法。然而，该方法在检查OSEK/VDX应用程序时执行的效率很低，因为OSEK/VDX应用程序持有许多循环，特别是它无法处理中断。在本文中，为了应用模型检查验证技术来检查实际的OSEK/VDX应用，我们开发并研究了一种基于众所周知的模型检查器Spin的替代方法。在我们的基于自旋的方法中，考虑了中断，并且使用了两种优化策略，通过减少状态空间和加速错误检测来提高方法的可扩展性和效率。我们在一系列实验的基础上研究了基于自旋的方法。实验结果表明，该方法对于验证所开发的OSEK/VDX应用程序具有许多循环和中断是一种有效的技术。
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.