2026-10-04T19:18:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2831 2024-03-06T09:28:45Z ddc:004 open_access

METAMOC: Modular Execution Time Analysis using Model Checking Dalsgaard, Andreas E. Olesen, Mads Chr. Toft, Martin Hansen, René Rydhof Larsen, Kim Guldstrand WCET analysis timed automata model checking UPPAAL 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 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älardalen WCET benchmark programs show that taking caching into account yields much tighter WCETs than without modelling caches, and that METAMOC is a sufficiently fast and versatile approach for WCET analysis. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andreas E. Dalsgaard and Mads Chr. Olesen and Martin Toft and René Rydhof Hansen and Kim Guldstrand Larsen 2010 Is Part Of OASIcs, Volume 15, 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.WCET.2010.113 urn:nbn:de:0030-drops-28319 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2010.113 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode