A Stepwise Symbolic Execution Testing Method And Implementation For OSEK/VDX Multitasking Applications

OSEK/VDX is a software development standard for vehicle software systems aimed at addressing the issues of reusability and portability of software developed by different manufacturers.With the growth of intelligent functions in vehicle software,applications developed based on the OSEK/VDX standard are becoming increasingly complex.Therefore,developers face a significant challenge how to high-efficiently and automatically testing OSEK/VDX multitasking applications to improve their reliability.Developers often use random testing as an effective automated detection solution,but a large number of tests are redundant in random testing,and there are problems with low testing efficiency and inadequate coverage.In recent years,the detection capabilities of symbolic execution have made significant progress,and symbolic execution-based testing methods have been widely applied in the detection practices of different types of programs,such as the hybrid symbolic execution testing method.However,existing symbolic execution-based testing methods are targeted at sequential programs,while OSEK/VDX applications are concurrent programs based on deterministic schedulers,so these methods cannot be directly applied to test OSEK/VDX applications,and there are problems with SMT solver solving capacity limitations and path explosion in existing symbolic executionbased testing methods.To achieve efficient and automated testing of OSEK/VDX multitasking applications,this paper proposes a stepwise symbolic execution testing method.Firstly,this method translates the target OSEK/VDX application program into an equivalent sequential model through multitasking sequentialization calculation,so that existing testing methods can be applied to test OSEK/VDX application.Secondly,the stepwise symbolic execution method combines bounded random testing and symbolic execution,collects path constraints in a breadth first search manner,and alleviates the capacity limitations of SMT solvers,while enhancing the precision of generating test cases via random testing with constraint conditions,further improving path coverage and testing efficiency.Finally,optimization processing is performed on the path explosion problem caused by loops in the OSEK/VDX program,as well as the unsymbolizable external function call problem,enhancing the performance of the stepwise symbolic execution testing method.Based on the proposed method,this paper developed an automated tool for testing OSEK/VDX multitasking applications,which receives the source files and configuration files of OSEK/VDX application as input and outputs a set of test cases and corresponding execution paths.To evaluate the performance of this method,this paper conducted a series of experiments on OSEK/VDX multitasking applications with different numbers of variables,branches,and loops using the tool,and compared traditional random testing and hybrid symbolic execution testing methods.The experimental results show that the proposed stepwise symbolic execution testing method can significantly improve coverage and testing efficiency contrasted to the compared methods,and is an effective method to ensure the reliability of OSEK/VDX multitasking applications.