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.2009.2281
URN: urn:nbn:de:0030-drops-22810
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2009/2281/
Go to the corresponding OASIcs Volume Portal

Huber, Benedikt ; Schoeberl, Martin

Comparison of Implicit Path Enumeration and Model Checking Based WCET Analysis

pdf-format:
Huber.2281.pdf (0.2 MB)

Abstract

In this paper, we present our new worst-case execution time (WCET) analysis tool for Java processors, supporting both implicit path enumeration (IPET) and model checking based execution time estimation. Even though model checking is significantly more expensive than IPET, it simplifies accurate modeling of pipelines and caches. Experimental results using the UPPAAL model checker indicate that model checking is fast enough for typical tasks in embedded applications, though large loop bounds may lead to long analysis times. To obtain a tool which is able to cope with larger applications, we recommend to use model checking for more important code fragments, and combine it with the IPET approach.

BibTeX - Entry

@InProceedings{huber_et_al:OASIcs:2009:2281,
  author =	{Benedikt Huber and Martin Schoeberl},
  title =	{{Comparison of Implicit Path Enumeration and Model Checking Based WCET Analysis}},
  booktitle =	{9th International Workshop on Worst-Case Execution Time Analysis (WCET'09) },
  pages =	{1--12},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-14-9},
  ISSN =	{2190-6807},
  year =	{2009},
  volume =	{10},
  editor =	{Niklas Holsti},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2281},
  URN =		{urn:nbn:de:0030-drops-22810},
  doi =		{10.4230/OASIcs.WCET.2009.2281},
  note =	{also published in print by Austrian Computer Society (OCG) with ISBN 978-3-85403-252-6},
  annote =	{Keywords: WCET analysis, model checking, IPET, Java, JOP, UPPAAL}
}

Keywords: WCET analysis, model checking, IPET, Java, JOP, UPPAAL
Collection: 9th International Workshop on Worst-Case Execution Time Analysis (WCET'09)
Issue Date: 2009
Date of publication: 26.11.2009

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