stefanabstract.shtml
Abstract  lic thesis Stefan Bygde

Static WCET Analysis based on Abstract Interpretation and Counting of Elements
In a realtime system, it is crucial to ensure that all tasks of the system hold their deadlines. A missed deadline in a realtime system means that the system has not been able to function correctly. If the system is safety critical, this can lead to disaster. To ensure that all tasks keep their deadlines, the WorstCase Execution Time (WCET) of these tasks has to be known. This can be done by measuring the execution times of a task, however, this is inflexible, time consuming and in general not safe (i.e., the worstcasemight not be found). Unless the task is measured with all possible input combinations and configurations, which is in most cases out of the question, there is no way to guarantee that the longest measured time actually corresponds to the real worst case.
Static analysis analyses a safe model of the hardware together with the source or object code of a program to derive an estimate of theWCET. This estimate is guaranteed to be equal to or greater than the real WCET. This is done by making calculations which in all steps make sure that the time is exactly or conservatively estimated. In many cases, however, the execution time of a task or a program is highly dependent on the given input. Thus, the estimated worst case may correspond to some input or configuration which is rarely (or never) used in practice. For such systems, where execution time is highly input dependent, a more accurate timing analysis which take input into consideration is desired.
In this thesis we present a framework based on abstract interpretation and counting of possible semantic states of a program. This is a general method of WCET analysis, which is language independent and platform independent.
The two main applications of this framework are a loop bound analysis and a parametric analysis. The loop bound analysis can be used to quickly find upper bounds for loops in a program while the parametric framework provides an inputdependent estimation of theWCET. The inputdependent estimation can give much more accurate estimates if the input is known at runtime.
