autoC: an efficient translator for model checking deterministic scheduler based OSEK/VDX applications  

作　　者：Haitao ZHANG Zhuo CHENG Guoqiang LI Shaoying LIU 

机构地区：[1]School of Information Science and Engineering, Lanzhou University [2]School of Information Science, Japan Advanced Institute of Science and Technology [3]School of Software, Shanghai Jiao Tong University [4]Faculty of Computer and Information Sciences, Hosei University

出　　处：《Science China(Information Sciences)》2018年第5期137-151,共15页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China (Grant Nos. 61602224, 61472240);Fundamental Research Funds for the Central Universities (Grant Nos. lzujbky-2016-142, lzujbky-2016-k07)

摘　　要：The OSEK/VDX automotive OS standard has been widely adopted by many automobile man- ufacturers, such as BMW and TOYOTA, as the basis for designing and implementing a vehicle-mounted OS. With the increasing functionalities in vehicles, more and more multi-task applications are developed based on the OSEK/VDX OS. Currently, ensuring the reliability of the developed applications is becoming a challenge for developers. As to ensure the reliability of OSEK/VDX applications, model checking as a potential solution has attracted great attention in the automotive industry. However, existing model check- ers are often unable to verify a large-scale OSEK/VDX application that consists of many tasks, since the corresponding application model too complex. To make existing model checkers more scalable in verifying large-scale OSEK/VDX applications, we describe a software tool named autoC to tackle this problem by automatically translating a multi-task OSEK/VDX application into an equivalent sequential model. We conducted a series of experiments to evaluate the efficiency of autoC. The experimental results show that autoC is not only capable of efficiently sequentializing OSEK/VDX applications, but also of improving the scalability and efficiency of existing model checkers in verifying large-scale OSEK/VDX applications.The OSEK/VDX automotive OS standard has been widely adopted by many automobile man- ufacturers, such as BMW and TOYOTA, as the basis for designing and implementing a vehicle-mounted OS. With the increasing functionalities in vehicles, more and more multi-task applications are developed based on the OSEK/VDX OS. Currently, ensuring the reliability of the developed applications is becoming a challenge for developers. As to ensure the reliability of OSEK/VDX applications, model checking as a potential solution has attracted great attention in the automotive industry. However, existing model check- ers are often unable to verify a large-scale OSEK/VDX application that consists of many tasks, since the corresponding application model too complex. To make existing model checkers more scalable in verifying large-scale OSEK/VDX applications, we describe a software tool named autoC to tackle this problem by automatically translating a multi-task OSEK/VDX application into an equivalent sequential model. We conducted a series of experiments to evaluate the efficiency of autoC. The experimental results show that autoC is not only capable of efficiently sequentializing OSEK/VDX applications, but also of improving the scalability and efficiency of existing model checkers in verifying large-scale OSEK/VDX applications.

关 键 词：OSEK/VDX application deterministic scheduler software formal method model checking sequentialization 

分 类 号：U463.6[机械工程—车辆工程]