Bounded Model Checking For Concurrent Behavior Based On Scheduler

With the advancement of the automobile manufacturing technology, demands for theauxiliary functions of vehicles have also increased sharply and tended to bediversified, which have greatly stimulated the application and development ofelectronic techniques in automobile industry. However, not all of the electronic partsmanufacturers use the same production standard, there exist extremely complexcorrespondence and cooperation between different electronic parts. OSEK/VDX, as astandard for automobile industry, has been proposed by Germany and Franceautomobile manufacturers and applied in many automobile systems to normalize thecorrespondence and cooperation. Especially, in OSEK/VDX OS, which task to be runis determined by scheduler, in addition, tasks can send service commands to requestscheduler for responding to its particular behaviors, such as terminating itself,activating a task and chaining a task. Thus, there may exist a potential risk which iscaused by an unreasonable dispatching when tasks run in the system. Therefore, howto check the safety property of a multi-task software based on automobileOSEK/VDX OS has become very difficult and crucial.Model checking, as a traditional technique, has been applied to checking multi-tasksoftware, however, suffers from combinatorial state space explosion when verifyingcomplex multi-task software. Recently, a new technique called bounded modelchecking (BMC) has been proposed to overcome the state explosion problem and hasbeen successfully applied to verify the multi-task software. There are many efficientand reliable techniques based on BMC have been proposed to check safety property ofmulti-task software, e.g., Ganai and Gupta describe a verification framework for BMCto extract high-level design information from an extended finite state machine(EFSM), and several techniques have been employed to simplify the BMC problem,they also describe a lazy method for modeling multi-task concurrent software usingshared variables. Grumberg et al. propose a method based on SAT and BMC to checka multi-task system with a series of under-approximated models. However, thesetechniques focus on the tasks’ current behaviors, the scheduler’s behaviors are notconsidered in verification process. Therefore, these techniques are not able to checkthe safety property of a software in which tasks are dispatched by a scheduler to beexecuted. In our article, we propose an approach to check the safety property of multi-tasksoftware in which tasks are dispatched by fixed priority scheduler (FPS) based onOSEK/VDX OS. In order to accomplish our research purpose, firstly, we analyze thedispatching behaviors of FPS based on OSEK/VDX OS, and then we use an extendedfinite state machine to establish a model for FPS and describe tasks’ behaviors.Especially, our FPS model can respond to three types of service commands which aresent by tasks in order to realize tasks’ particular requests, such as terminating a task,activating a task and chaining a task. Furthermore, as to obtain the execution paths oftasks that are dispatched by FPS, we establish a k-step execution tree to represent allof the possible execution paths. In the execution tree, each possible execution path isfrom root-node to one of leaf-nodes and the total amount of execution paths is equalto the total amount of leaf-nodes. In order to ensure each service command whichexists in branches of task can be responded by FPS, we insert FPS model into eachnode of execution tree for obtain all of the dispatching execution paths.Based on execution tree, we propose two strategies to extract execution paths inwhich BMC is employed to generate the verification conditions (VCs) based on ourexecution tree. In addition, Yices which is satisfiability modulo theories (SMT) solverand capable of handling large and propositionally complex formulas in a richcombination of theories is used to check the generated VCs with verification propertyformula and return the verification results. Finally, we implement two types of toolsaccording to our two strategies of extracting execution paths based on execution treeto evaluate our approach. Using our tools, we can directly get the k-step transitionsystem M which is composed of each execution path’s VCs based on FPS dispatching,furthermore, the k-step transition system M can be translated into Yices file with ourtools. We also carry out some relevant experiments with our tools, results show thatour approach can efficiently check the safety property of multi-task software in whichtasks are dispatched by FPS.