Modular Execution Time Analysis using Model Checking: METAMOC

Student thesis: Master thesis (including HD thesis)

  • Andreas Engelbredt Dalsgaard
  • Mads Chr. Olesen
  • Martin Toft
2. term, Computer Science, Master (Master Programme)
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 WCET 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 implementation, in order to add support for additional hardware platforms. Experiments with the implementation show that the principles used in the method work very well, and that taking especially caching into account is worth the effort.
LanguageEnglish
Publication date2009
Number of pages108
Publishing institutionDepartment of Computer Science
ID: 17626018