A master thesis from Aalborg University
Modular Execution Time Analysis using Model Checking: METAMOC
Author(s)
Term
2. term
Education
Publication year
2009
Submitted on
2009-06-01
Pages
108 pages
Abstract
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.
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.