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

Prantl, Adrian ; Knoop, Jens ; Kirner, Raimund ; Kadlec, Albrecht ; Schordan, Markus

From Trusted Annotations to Verified Knowledge

pdf-format:
Prantl.2282.pdf (0.2 MB)

Abstract

WCET analyzers commonly rely on user-provided annotations such as loop bounds, recursion depths, region- and program constants. This reliance on user-provided annotations has an important drawback. It introduces a Trusted Annotation Basis into WCET analysis without any guarantee that the user-provided annotations are safe, let alone sharp. Hence, safety and accuracy of a WCET analysis cannot be formally established. In this paper we propose a uniform approach, which reduces the trusted annotation base to a minimum, while simultaneously yielding sharper (tighter) time bounds. Fundamental to our approach is to apply model checking in concert with other more inexpensive program analysis techniques, and the coordinated application of two algorithms for Binary Tightening and Binary Widening, which control the application of the model checker and hence the computational costs of the approach. Though in this paper we focus on the control of model checking by Binary Tightening and Widening, this is embedded into a more general approach in which we apply an array of analysis methods of increasing power and computational complexity for proving or disproving relevant time bounds of a program. First practical experiences using the sample programs of the Mälardalen benchmark suite demonstrate the usefulness of the overall approach. In fact, for most of these benchmarks we were able to empty the trusted annotation base completely, and to tighten the computed WCET considerably.

BibTeX - Entry

@InProceedings{prantl_et_al:OASIcs:2009:2282,
  author =	{Adrian Prantl and Jens Knoop and Raimund Kirner and Albrecht Kadlec and Markus Schordan},
  title =	{{From Trusted Annotations to Verified Knowledge}},
  booktitle =	{9th International Workshop on Worst-Case Execution Time Analysis (WCET'09) },
  pages =	{1--11},
  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/2282},
  URN =		{urn:nbn:de:0030-drops-22828},
  doi =		{10.4230/OASIcs.WCET.2009.2282},
  note =	{also published in print by Austrian Computer Society (OCG) with ISBN 978-3-85403-252-6},
  annote =	{Keywords: WCET analysis, annotations, binary tightening, binary widening, model checking, CBMC}
}

Keywords: WCET analysis, annotations, binary tightening, binary widening, model checking, CBMC
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