Modular Execution Time Analysis using Model Checking (METAMOC)

Studenteropgave: Speciale (inkl. HD afgangsprojekt)

  • Andreas Engelbredt Dalsgaard
  • Mads Chr. Olesen
  • Martin Toft
4. semester, Datalogi, Kandidat (Kandidatuddannelse)
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.
Udgivelsesdatojun. 2009
ID: 61075281