Modular Execution Time Analysis using Model Checking (METAMOC)
Authors
Dalsgaard, Andreas Engelbredt ; Olesen, Mads Chr. ; Toft, Martin
Term
4. term
Education
Publication year
2009
Abstract
Værste udførelsestid (WCET) er den maksimale tid, et stykke software kan bruge på at køre. At kende en sikker og skarp (dvs. tæt) øvre grænse er afgørende for planlægning i realtidssystemer, fordi det påvirker både pålidelighed og effektiv udnyttelse af ressourcer. Dette speciale præsenterer METAMOC, en fleksibel WCET-analyseteknik, der kombinerer modelkontrol (model checking) og statisk analyse. Modelkontrol gennemgår systematisk relevante program- og hardwareforløb, mens statisk analyse vurderer koden uden at køre den. METAMOC er organiseret i fire løst koblede delanalyser, hvilket gør det nemt at tilpasse og genbruge dele af metoden. Metoden tager højde for hardwareegenskaber, der påvirker køretid, især cache og pipelining, som kan gøre koden hurtigere eller langsommere på komplekse måder. For at demonstrere METAMOC blev den implementeret til ARM920T-processoren og testet på de fleste WCET-benchmarkprogrammer fra Mälardalen Real-Time Research Center. Forsøgene viser, at principperne i metoden fungerer godt i praksis, og at det især er umagen værd at tage cache i betragtning.
Worst-case execution time (WCET) is the maximum time a piece of software can take to run. Knowing a safe and tight upper bound is essential for scheduling in real-time systems because it affects both reliability and efficient use of resources. This thesis introduces METAMOC, a flexible WCET analysis method that combines model checking and static analysis. Model checking systematically explores relevant program and hardware behaviors, while static analysis reasons about code without running it. METAMOC is structured into four loosely coupled sub-analyses, making it easier to adapt and reuse parts of the method. The method accounts for hardware features that strongly influence execution time, especially caches and pipelines, which can speed up or slow down code in complex ways. To demonstrate METAMOC, it was implemented for the ARM920T processor and tested on most of the WCET benchmark programs from the Mälardalen Real-Time Research Center. The experiments show that the principles behind the method work well in practice, and that explicitly considering caching is worth the effort.
[This abstract was generated with the help of AI]
Documents