Research On Worst-Case Execution Time Analysis Techniques Of Real-Time Systems

Schedulability analysis and Worst-Case Execution Time (WCET) analysis are two major tasks of timing validation of real-time systems. The purpose of WCET analysis is to obtain the execution time of a real-time task in the worst-case, and its results serve as the input to schedulability analysis. Static analysis, which includes processor behavior analysis, flow analysis, and WCET calculation, is usually adopted to guarantee safe results in hard real-time systems. Currently Implicit Path Enumeration is the dominating technique in WCET calculation, but the drawback of this technique is limited expressiveness in describing program control flow, which further limits the techniques used to conduct processor behavior analysis. Cache analysis has always been a hard task in processor behavior analysis. Abstract Interpretation based methods have gained predominance in analyzing caches with LRU replacement policy, but analysis methods for other policies, such as FIFO, are still immature. With the trend of multicore processors, shared cache becomes a prevalent Cache architecture. Fine-grained sharing of caches among different cores makes the timing behavior of tasks unpredictable, which brings great challenges to WCET analysis. With the development of WCET analysis techniques, usability issues have also become a major concern.Given the above research background, we conducted research on WCET calculation, single-core and multi-core Cache analysis, and WCET analysis of real-time operating systems in this thesis. Detailed contributions are as follows:(1) A new WCET calculation method based on model checking was developed, and the transformation semantics from a program to the corresponding automaton was designed. The ability of searching optimal solutions of model checking is leveraged in WCET calculation for better analysis precision. We used different model checkers in the analysis with a discussion on the time and space scalability issues. Usage guidelines of WCET analysis based on model checking were also given.(2) A single-core cache analysis method based on the idea of branch cutting was put forward in this thesis. First, model checking was used to model the behavior of FIFO caches; then a method that implements the idea of branch cutting was designed to tackle the state space explosion problem in WCET analysis based on model checking. By cutting off the program branches that satisfy specific criteria, the method can efficiently improve the analysis performance and scalability without sacrificing analysis precision.(3) A model checking based method to analyze shared caches in multi-cores was designed in this thesis. The key point of analyzing shared caches is to precisely analyze the inter-core interferences. Existing techniques only take address-related conflicts into account, thus result in large overestimation. We used model checker to model shared cache behaviors, and experiment results show that the analysis precision is greatly improved, since the timing order of cache conflicts are captured in the models.(4) We also conducted research on WCET analysis of theμC/OS-Ⅱreal-time operating system (RTOS). RTOS code is control-intensive, which makes them different from application code in terms of timing properties. The system calls and disabled interrupt regions ofμC/OS-Ⅱare analyzed using static methods, and the analysis precision and existing problems in static WCET analysis of RTOS are analyzed intensively. The results of the analysis can directly serve as a comprehensive and quantitative description of the timing properties ofμC/OS-Ⅱ, which is helpful to RTOS users to understand the real-time performance of the operating system, and can provide useful information for system designers in improving system performance as well.(5) A static WCET analysis tool that supports multi-core architecture was developed based on Chronos-a WCET analysis prototype developed by National University of Singapore. Techniques on WCET calculation based on model checking, single-core cache analysis with branch cutting, multi-core shared cache analysis, and static analysis of RTOS are implemented in this tool to verify the techniques designed in this thesis.To summarize, research on static WCET analysis based on model checking is conducted in this thesis, and experiment results show that the techniques can achieve better precision. Experience and problems in static analysis of RTOS are also explored. The work of this thesis could provide reference value to researches on static WCET analysis and usability aspects of WCET analysis.