Document Open Access Logo

DELOOP: Automatic Flow Facts Computation Using Dynamic Symbolic Execution

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

PDF

File

Thumbnail PDF
PDF
OASIcs.WCET.2022.3.pdf
  • Filesize: 0.66 MB
  • 12 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computer systems organization → Real-time system specification
  • Software and its engineering → Real-time systems software
Keywords
  • Real-Time
  • WCET
  • Symbolic execution

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 Get BibTex

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) https://doi.org/10.4230/OASIcs.WCET.2022.3

Author Details

Hazem Abaza
  • TU Dortmund, Germany
Zain Alabedin Haj Hammadeh
  • Institute for Software Technology, German Aerospace Center (DLR), Braunschweig, Germany
Daniel Lüdtke
  • Institute for Software Technology, German Aerospace Center (DLR), Braunschweig, Germany

Acknowledgements

The authors thank Prof. Dr. Heiko Falk for his valuable feedback. Also, they thank Patrick Kenny for proof-reading the paper.

References

  1. Avast. RetDec. https://github.com/avast/retdec. [accessed May 03, 2022].
  2. Clément Ballabriga, Hugues Cassé, Christine Rochange, and Pascal Sainrat. OTAWA: an open toolbox for adaptive WCET analysis. In IFIP International Workshop on Software Technolgies for Embedded and Ubiquitous Systems, pages 35-46. Springer, 2010. Google Scholar
  3. BINARYNINJA. Binary Ninja. https://binary.ninja/. [accessed May 03, 2022].
  4. Robin David, Sébastien Bardin, Thanh Dinh Ta, Laurent Mounier, Josselin Feist, Marie-Laure Potet, and Jean-Yves Marion. Binsec/se: A dynamic symbolic execution toolkit for binary-level analysis. In 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER), volume 1, pages 653-656, 2016. URL: https://doi.org/10.1109/SANER.2016.43.
  5. Marianne de Michiel, Armelle Bonenfant, Hugues Casse, and Pascal Sainrat. Static loop bound analysis of C programs based on flow analysis and abstract interpretation. In 2008 14th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, pages 161-166, 2008. URL: https://doi.org/10.1109/RTCSA.2008.53.
  6. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  7. Leonardo De Moura and Nikolaj Bjørner. Satisfiability modulo theories: Introduction and applications. Commun. ACM, 54(9):69-77, September 2011. URL: https://doi.org/10.1145/1995376.1995394.
  8. Andreas Ermedahl and Jakob Engblom. Execution time analysis for embedded real-time systems. International Journal on Software Tools for Technology Transfer, 4:437-455, 2007. Google Scholar
  9. Andreas Ermedahl, Christer Sandberg, Jan Gustafsson, Stefan Bygde, and Björn Lisper. Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis. In Christine Rochange, editor, 7th International Workshop on Worst-Case Execution Time Analysis (WCET'07), volume 6 of OpenAccess Series in Informatics (OASIcs), Dagstuhl, Germany, 2007. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/OASIcs.WCET.2007.1194.
  10. Mohamed Fayad and Douglas C. Schmidt. Object-oriented application frameworks. Commun. ACM, 40(10):32-38, October 1997. URL: https://doi.org/10.1145/262793.262798.
  11. Christian Ferdinand and Reinhold Heckmann. aiT: Worst-case execution time prediction by static program analysis. In Renè Jacquart, editor, Building the Information Society, pages 377-383, Boston, MA, 2004. Springer US. Google Scholar
  12. Jorge Garrido, Daniel Brosnan, Juan A. de la Puente, Alejandro Alonso, and Juan Zamorano. Analysis of WCET in an experimental satellite software development. In Tullio Vardanega, editor, 12th International Workshop on Worst-Case Execution Time Analysis, volume 23 of OpenAccess Series in Informatics (OASIcs), pages 81-90, Dagstuhl, Germany, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/OASIcs.WCET.2012.81.
  13. Jorge Garrido, Juan Zamorano, and Juan A. de la Puente. Static analysis of WCET in a satellite software subsystem. In Claire Maiza, editor, 13th International Workshop on Worst-Case Execution Time Analysis, volume 30 of OpenAccess Series in Informatics (OASIcs), pages 87-96, Dagstuhl, Germany, 2013. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/OASIcs.WCET.2013.87.
  14. German Aerospace Center (DLR). Tasking Framework. https://github.com/DLR-SC/tasking-framework. [accessed May 03, 2022].
  15. Jan Gustafsson, Adam Betts, Andreas Ermedahl, and Björn Lisper. The Mälardalen WCET Benchmarks: Past, Present And Future. In Björn Lisper, editor, 10th International Workshop on Worst-Case Execution Time Analysis (WCET 2010), volume 15 of OpenAccess Series in Informatics (OASIcs), pages 136-146, Dagstuhl, Germany, 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. The printed version of the WCET'10 proceedings are published by OCG (www.ocg.at) - ISBN 978-3-85403-268-7. URL: https://doi.org/10.4230/OASIcs.WCET.2010.136.
  16. Jan Gustafsson, Andreas Ermedahl, Christer Sandberg, and Bjorn Lisper. Automatic derivation of loop bounds and infeasible paths for WCET analysis using abstract execution. In 2006 27th IEEE International Real-Time Systems Symposium (RTSS'06), pages 57-66, 2006. URL: https://doi.org/10.1109/RTSS.2006.12.
  17. Zain Alabedin Haj Hammadeh, Tobias Franz, Olaf Maibaum, Andreas Gerndt, and Daniel Lüdtke. Event-driven multithreading execution platform for real-time on-board software systems. In Proceedings of the 15th Annual Workshop on Operating Systems Platforms for Embedded Real-time Applications, pages 29-34, 2019. Google Scholar
  18. Julien Henry, Mihail Asavoae, David Monniaux, and Claire Maïza. How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. SIGPLAN Not., 49(5):43-52, June 2014. URL: https://doi.org/10.1145/2666357.2597817.
  19. Hajer Herbegue, Hugues Cassé, Mamoun Filali, and Christine Rochange. Hardware architecture specification and constraint-based WCET computation. In 2013 8th IEEE International Symposium on Industrial Embedded Systems (SIES), pages 259-268. IEEE, 2013. Google Scholar
  20. Donald B Johnson. Finding all the elementary circuits of a directed graph. SIAM Journal on Computing, 4(1):77-84, 1975. Google Scholar
  21. Andreas Lund, Zain Alabedin Haj Hammadeh, Patrick Kenny, Vishav Vishav, Andrii Kovalov, Hannes Watolla, Andreas Gerndt, and Daniel Lüdtke. ScOSA system software: the reliable and scalable middleware for a heterogeneous and distributed on-board computer architecture. CEAS Space Journal, May 2021. URL: https://doi.org/10.1007/s12567-021-00371-7.
  22. RAPITASytems. RapiTime. https://www.rapitasystems.com/products/rapitime. [accessed May 03, 2022].
  23. Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Erwan Jahier, Nicolas Halbwachs, Fabienne Carrier, Mihail Asavoae, and Rémy Boutonnet. Improving WCET evaluation using linear relation analysis. Leibniz Transactions on Embedded Systems, 6(1):02:1-02:28, February 2019. URL: https://doi.org/10.4230/LITES-v006-i001-a002.
  24. Jordy Ruiz and Hugues Cassé. Using SMT solving for the lookup of infeasible paths in binary programs. In Francisco J. Cazorla, editor, 15th International Workshop on Worst-Case Execution Time Analysis ( WCET 2015), volume 47 of OpenAccess Series in Informatics (OASIcs), pages 95-104, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/OASIcs.WCET.2015.95.
  25. Stephan Theil, N Ammann, Franz Andert, Tobias Franz, Hans Krüger, Hannah Lehner, Martin Lingenauber, Daniel Lüdtke, Bolko Maass, Carsten Paproth, et al. ATON (autonomous terrain-based optical navigation) for exploration missions: recent flight test results. CEAS Space Journal, 10(3):325-341, 2018. Google Scholar
  26. Rick Veens. Adding support for static WCET analysis to LLVM, 2018. Master’s thesis. URL: https://research.tue.nl/en/studentTheses/adding-support-for-static-wcet-analysis-to-llvm.
  27. Alexey Vishnyakov, Andrey Fedotov, Daniil Kuts, Alexander Novikov, Darya Parygina, Eli Kobrin, Vlada Logunova, Pavel Belecky, and Shamil Kurmangaleev. Sydr: Cutting edge dynamic symbolic execution. In 2020 Ivannikov Ispras Open Conference (ISPRAS), pages 46-54, 2020. URL: https://doi.org/10.1109/ISPRAS51486.2020.00014.
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact