METAMOC: Modular Execution Time Analysis using Model Checking

Safe and tight worst-case execution times (WCETs) are important when scheduling hard realtime 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 model of the hardware platform and model checked for the WCET. Through support for the platforms ARM7, ARM9 and ATMEL AVR 8-bit, the modularity and retargetability of the method are demonstrated, as only the pipeline needs to be remodelled. Hardware modelling is performed in a state-of-the-art graphical modelling environment. Experiments on the M

• Type: Journal
• Year: 2010
• Where: WCET
• Authors: Andreas E. Dalsgaard, Mads Chr. Olesen, Martin Toft, René Rydhof Hansen, Kim Guldstrand Larsen
• Keywords: Graphical Modelling Environment, Model, Software Engineering, Tight Worst-case Execution, WCET 2010