License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WCET.2022.3
URN: urn:nbn:de:0030-drops-166256
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16625/
Go to the corresponding OASIcs Volume Portal

Abaza, Hazem ; Haj Hammadeh, Zain Alabedin ; Lüdtke, Daniel

DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution

pdf-format:
OASIcs-WCET-2022-3.pdf (0.7 MB)

Abstract

Constructing a complete control-flow graph (CGF) and computing upper bounds on loops of a computing system are essential to safely estimate the worst-case execution time (WCET) of real-time tasks. WCETs are required for verifying the timing requirements of a real-time computing system. Therefore, we propose an analysis using dynamic symbolic execution (DSE) that detects and computes upper bounds on the loops, and resolves indirect jumps. The proposed analysis constructs and initializes memory models, then it uses a satisfiability modulo theories (SMT) solver to symbolically execute the instructions. The analysis showed higher precision in bounding loops of the Mälardalen benchmarks comparing to SWEET and oRange. We integrated our analysis with the OTAWA toolbox for performing a WCET analysis. Then, we used the proposed analysis for estimating the WCET of functions in a use case inspired by an aerospace project.

BibTeX - Entry

@InProceedings{abaza_et_al:OASIcs.WCET.2022.3,
  author =	{Abaza, Hazem and Haj Hammadeh, Zain Alabedin and L\"{u}dtke, Daniel},
  title =	{{DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution}},
  booktitle =	{20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022)},
  pages =	{3:1--3:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-244-0},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{103},
  editor =	{Ballabriga, Cl\'{e}ment},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16625},
  URN =		{urn:nbn:de:0030-drops-166256},
  doi =		{10.4230/OASIcs.WCET.2022.3},
  annote =	{Keywords: Real-Time, WCET, Symbolic execution}
}

Keywords: Real-Time, WCET, Symbolic execution
Collection: 20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022)
Issue Date: 2022
Date of publication: 14.07.2022

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