1 Search Results for "Abaza, Hazem"


Document
DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution

Authors: Hazem Abaza, Zain Alabedin Haj Hammadeh, and Daniel Lüdtke

Published in: OASIcs, Volume 103, 20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022)


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.

Cite as

Hazem Abaza, Zain Alabedin Haj Hammadeh, and Daniel Lüdtke. DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution. In 20th International Workshop on Worst-Case Execution Time Analysis (WCET 2022). Open Access Series in Informatics (OASIcs), Volume 103, pp. 3:1-3:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2022.3},
  URN =		{urn:nbn:de:0030-drops-166256},
  doi =		{10.4230/OASIcs.WCET.2022.3},
  annote =	{Keywords: Real-Time, WCET, Symbolic execution}
}
  • Refine by Author
  • 1 Abaza, Hazem
  • 1 Haj Hammadeh, Zain Alabedin
  • 1 Lüdtke, Daniel

  • Refine by Classification
  • 1 Computer systems organization → Real-time system specification
  • 1 Software and its engineering → Real-time systems software

  • Refine by Keyword
  • 1 Real-Time
  • 1 Symbolic execution
  • 1 WCET

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail