Pages including appendices:

The ability to determine safe and sharp worst-case execution time (WCET) for processes is very important when scheduling real-time systems, as it influences the reliability and efficiency of the resulting systems. This thesis presents METAMOC, a flexible WCET analysis method based on model checking and static analysis that determines safe and sharp WCETs for processes running on hardware platforms featuring caching and pipelining. The method is divided into four loosely coupled sub-analyses. To demonstrate and evaluate the method, it is implemented for the ARM920T processor and tested successfully on most of the WCET benchmark programs from Mälardalen Real-Time Research Center. The flexibilty of the method allows for easy replacement and reuse of parts of the implemen-tation, in order to add support for additional hardware platforms. Experiments with the implemen-tation show that the principles used in the method work very well, and that taking especially caching into account is worth the effort. The content of this report is freely available, but publication (with source reference) may only be made with the approval of the authors. 4 Preface The present report is our master's thesis, which documents the results of our work during the spring semester of 2009. The thesis is on the topic of formal systems and marks the completion of a specialisation year in the Distribute