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.
@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/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} }
Feedback for Dagstuhl Publishing