License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WCET.2010.113
URN: urn:nbn:de:0030-drops-28319
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2831/
Go to the corresponding OASIcs Volume Portal

Dalsgaard, Andreas E. ; Olesen, Mads Chr. ; Toft, Martin ; Hansen, René Rydhof ; Larsen, Kim Guldstrand

METAMOC: Modular Execution Time Analysis using Model Checking

pdf-format:
13.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{dalsgaard_et_al:OASIcs:2010:2831,
  author =	{Andreas E. Dalsgaard and Mads Chr. Olesen and Martin Toft and Ren{\'e} Rydhof Hansen and Kim Guldstrand Larsen},
  title =	{{METAMOC: Modular Execution Time Analysis using Model Checking}},
  booktitle =	{10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010)},
  pages =	{113--123},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-21-7},
  ISSN =	{2190-6807},
  year =	{2010},
  volume =	{15},
  editor =	{Bj{\"o}rn Lisper},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2831},
  URN =		{urn:nbn:de:0030-drops-28319},
  doi =		{10.4230/OASIcs.WCET.2010.113},
  note =	{The printed version of the WCET'10 proceedings are published by OCG (www.ocg.at) - ISBN 978-3-85403-268-7},
  annote =	{Keywords: WCET analysis, timed automata, model checking, UPPAAL}
}

Keywords: WCET analysis, timed automata, model checking, UPPAAL
Collection: 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010)
Issue Date: 2010
Date of publication: 26.11.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI