License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WCET.2013.53
URN: urn:nbn:de:0030-drops-41225
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4122/
Go to the corresponding OASIcs Volume Portal

Biere, Armin ; Knoop, Jens ; Kovács, Laura ; Zwirchmayr, Jakob

The Auspicious Couple: Symbolic Execution and WCET Analysis

pdf-format:
7.pdf (0.4 MB)

Abstract

We have recently shown that symbolic execution together with the implicit path enumeration technique can successfully be applied in the Worst-Case Execution Time (WCET) analysis of programs. Symbolic
execution offers a precise framework for program analysis and tracks complex program properties by analyzing single program paths in isolation. This path-wise program exploration of symbolic execution is, however, computationally expensive, which often prevents full symbolic analysis of larger applications: the number of paths in a program increases exponentially with the number of conditionals, a situation denoted as the path explosion problem. Therefore, for applying symbolic execution in the timing analysis of programs, we propose to use WCET analysis as a guidance for symbolic execution in order to avoid full symbolic coverage of the program. By focusing only on paths or program fragments that are relevant for WCET analysis, we keep the computational costs of symbolic execution low. Our WCET analysis also profits from the precise results derived via symbolic execution. In this article we describe how use-cases of symbolic execution are materialized in the r-TuBound toolchain
and present new applications of WCET-guided symbolic execution for WCET analysis. The new applications of selective symbolic execution are based on reducing the effort of symbolic analysis by focusing
only on relevant program fragments. By using partial symbolic program coverage obtained by selective symbolic execution, we improve the WCET analysis and keep the effort for symbolic execution low.

BibTeX - Entry

@InProceedings{biere_et_al:OASIcs:2013:4122,
  author =	{Armin Biere and Jens Knoop and Laura Kov{\'a}cs and Jakob Zwirchmayr},
  title =	{{The Auspicious Couple: Symbolic Execution and WCET Analysis}},
  booktitle =	{13th International Workshop on Worst-Case Execution Time Analysis},
  pages =	{53--63},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-54-5},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{30},
  editor =	{Claire Maiza},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4122},
  URN =		{urn:nbn:de:0030-drops-41225},
  doi =		{10.4230/OASIcs.WCET.2013.53},
  annote =	{Keywords: WCET analysis, Symbolic execution, WCET refinement, Flow Facts}
}

Keywords: WCET analysis, Symbolic execution, WCET refinement, Flow Facts
Collection: 13th International Workshop on Worst-Case Execution Time Analysis
Issue Date: 2013
Date of publication: 08.07.2013

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