| As a standard of distributed real-time operating system,OSEK/VDX has been widely adopted by automotive electronics industries.In order to improve the overall performance of the car,the design of the application program tends to be parallelized and complicated.The correctness of OSEK/VDX programs has received more and more attention.Previous verification methods for the OSEK/VDX application are testing and model checking.However,because of uncertainties and interactive complexity of the parallel program,the traditional verification methods have the problems of incomplete testing and state explosion in the verification process.To address these issues,this paper proposes a Petri net unfolding-based modeling and verification method of OSEK/VDX programs.The main contributions include:(1)A colored Petri net-based modeling method of OSEK/VDX key components and programs is presented.This method can construct the corresponding Petri net according to the specific application program.(2)Unfolding and reverse unfolding methods of the colored Petri net is proposed,and and the specific unfolding algorithm is given.Reverse unfolding of colored Petri nets is proposed to analyze the Petri net model of OSEK/VDX applications.Furthermore,the security problem of concurrent tasks in the system is converted into the coverage problem of Petri net target marking,and some problems of security verification of OSEK/VDX application is completed by the proposed reverse unfolding technology.Compared with the traditional verification method,this method can effectively reduce the state space to be searched and alleviate the state explosion problem.(3)The attribute of time is an important indicator that affects the security of OSEK/VDX applications.Time attribute is often ignored in traditional Petri net-based program verification methods.This paper introduces time attribute into the modeling method of OSEK/VDX application program based on Petri net,and introduce the verification problem of OSEK/VDX program correctness after considering the time attribute.Then,the problems of program deadlock,security of task and task synchronization are analyzed based on unfolding and reverse unfolding of colored Petri net. |
