METAMOC: Modular Execution Time Analysis using Model Checking

Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen & Kim Guldstrand Larsen
Safe and tight worst-case execution times (WCETs) are important when scheduling hard real-time systems. This paper presents METAMOC, a modular method, based on model checking and static analysis, that determines safe and tight WCETs for programs running on platforms featuring caching and pipelining. The method works by constructing a UPPAAL model of the program being analysed and annotating the model with information from an inter-procedural value analysis. The program model is then combined with a...