Formal method supporting for time modeling of real-time softwares
Hang Zhou · Journal of PLA University of Science and Technology · 2010
With the progress of non-functional properties research on real-time systems,to analyze the effect of software on system running time,a formal method was proposed to support time modeling of real-time softwares.By extending time information on Timed Communicating Sequential Process(Timed CSP),the execution time of instructions in real-time systems was mapped into the time of Timed CSP.The execution time of real-time softwares could be modeled and optimized using this formal method.A time optimal scheduling algorithm was proposed to estimate the reachability of Timed CSP and to figure out the time optimal path.The last instance shows that this formal method improves the accuracy and efficiency of the execution time calculation of real-time systems, and that the calculation results can be used to quantitatively analyze and optimize the execution time of real-time systems.