Modular Execution Time Analysis using Model Checking: METAMOC
Authors
Dalsgaard, Andreas Engelbredt ; Olesen, Mads Chr. ; Toft, Martin
Term
2. term
Education
Publication year
2009
Pages
108
Abstract
At kunne fastslå den maksimale tid et stykke software kan bruge på at køre (Worst-Case Execution Time, WCET) er afgørende for at planlægge realtidssystemer med stramme tidsfrister. Denne afhandling præsenterer METAMOC, en fleksibel metode, der kombinerer modelkontrol (model checking) og statisk analyse (teknikker der kan ræsonnere om programmer uden at køre dem) for at beregne WCET-værdier, der både er sikre (undervurderer aldrig) og skarpe (ikke unødigt konservative). METAMOC tager højde for processorfunktioner som cachehukommelse og pipelining, som kan påvirke tidsforbruget. Metoden er organiseret i fire løst koblede delanalyser, hvilket gør den modulær og nem at tilpasse; dele kan udskiftes og genbruges for at understøtte andre hardwareplatforme. For at demonstrere og evaluere den blev METAMOC implementeret til ARM920T-processoren og testet med succes på de fleste af WCET-benchmarkprogrammerne fra Mälardalen Real-Time Research Center. Forsøgene viser, at tilgangen fungerer godt, og at det især kan betale sig at inddrage caching.
Knowing the maximum time a piece of software can take to run (worst-case execution time, WCET) is essential for scheduling real-time systems that must meet strict deadlines. This thesis introduces METAMOC, a flexible method that combines model checking and static analysis (techniques that reason about programs without running them) to compute WCET values that are both safe (never underestimate) and sharp (not overly conservative). METAMOC handles processor features such as caching and pipelining, which can affect timing. The method is organized into four loosely coupled sub-analyses, making it modular and easier to adapt; parts can be replaced and reused to support additional hardware platforms. To demonstrate and evaluate it, we implemented METAMOC for the ARM920T processor and tested it successfully on most of the WCET benchmark programs from the Mälardalen Real-Time Research Center. The experiments show that the approach works well, and that explicitly accounting for caching is especially beneficial.
[This summary has been rewritten with the help of AI based on the project's original abstract]
Documents