Validating Static WCET Analysis: A Method and Its Application

Authors Wei-Tsun Sun, Eric Jenn, Hugues Cassé



PDF
Thumbnail PDF

File

OASIcs.WCET.2019.6.pdf
  • Filesize: 0.62 MB
  • 10 pages

Document Identifiers

Author Details

Wei-Tsun Sun
  • IRT Saint Exupéry, Toulouse, France
Eric Jenn
  • IRT Saint Exupéry, Toulouse, France
  • Thales AVS, Toulouse, France
Hugues Cassé
  • IRIT, Toulouse, France
  • University of Toulouse, France

Cite AsGet BibTex

Wei-Tsun Sun, Eric Jenn, and Hugues Cassé. Validating Static WCET Analysis: A Method and Its Application. In 19th International Workshop on Worst-Case Execution Time Analysis (WCET 2019). Open Access Series in Informatics (OASIcs), Volume 72, pp. 6:1-6:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/OASIcs.WCET.2019.6

Abstract

WCET analysis is a key activity in the development of safety critical real-time systems. Whether upper bounds on WCETs are obtained using static analysis or measurements, the confidence on the compliance of a system with its temporal requirements directly depends on the confidence on these estimations. Static WCET analysis based on abstract interpretation takes benefits from its formal foundations. However, it also strongly depends on the correctness of the underlying models. We hereby show how we have validated the version of the data flow static analyser of OTAWA applied to the AURIX TC275 target processor.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Real-time systems
Keywords
  • validation of WCET tools
  • ISS
  • nML

Metrics

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

References

  1. AURIX TC27x D-Step 32-Bit Single-Chip Microcontroller User’s Manual V2.2 2014-12. Google Scholar
  2. Hugues Cassé, Florian Birée, and Pascal Sainrat. Multi-architecture value analysis for machine code. In 13th International Workshop on Worst-Case Execution Time Analysis, pages pp-42, 2013. Google Scholar
  3. Hugues Cassé and Pascal Sainrat. OTAWA, a framework for experimenting WCET computations. In 3rd European Congress on Embedded Real-Time Software, volume 1, 2006. Google Scholar
  4. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM symposium on Principles of programming languages, pages 238-252, 1977. Google Scholar
  5. Thanh Nga Dang, Abhik Roychoudhury, Tulika Mitra, and Prabhat Mishra. Generating test programs to cover pipeline interactions. In 2009 46th ACM/IEEE Design Automation Conference, pages 142-147. IEEE, 2009. Google Scholar
  6. Christian Ferdinand and Reinhold Heckmann. ait: Worst-case execution time prediction by static program analysis. In Building the Information Society, pages 377-383. Springer, 2004. Google Scholar
  7. Christian Ferdinand, Reinhold Heckmann, Marc Langenbach, Florian Martin, Michael Schmidt, Henrik Theiling, Stephan Thesing, and Reinhard Wilhelm. Reliable and precise WCET determination for a real-life processor. In International Workshop on Embedded Software, page 469–485. Springer, 2001. Google Scholar
  8. Jan Gustafsson, Adam Betts, Andreas Ermedahl, and Björn Lisper. The Mälardalen WCET benchmarks: Past, present and future. In 10th International Workshop on Worst-Case Execution Time Analysis. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2010. Google Scholar
  9. Jan Gustafsson, Andreas Ermedahl, Björn Lisper, Christer Sandberg, and Linus Källberg. ALF-a language for WCET flow analysis. In 9th International Workshop on Worst-Case Execution Time Analysis (WCET'09). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2009. Google Scholar
  10. Xavier Leroy et al. The CompCert verified compiler. Documentation and user’s manual. INRIA Paris-Rocquencourt, 53, 2012. Google Scholar
  11. André Maroneze, Sandrine Blazy, David Pichardie, and Isabelle Puaut. A formally verified WCET estimation tool. In 14th International Workshop on Worst-Case Execution Time Analysis. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2014. Google Scholar
  12. Fadia Nemer, Hugues Cassé, Pascal Sainrat, Jean-Paul Bahsoun, and Marianne De Michiel. Papabench: a free real-time benchmark. In 6th International Workshop on Worst-Case Execution Time Analysis (WCET'06). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2006. Google Scholar
  13. Tahiry Ratsiambahotra, Hugues Cassé, and Pascal Sainrat. A versatile generator of instruction set simulators and disassemblers. In 2009 International Symposium on Performance Evaluation of Computer &Telecommunication Systems, volume 41, pages 65-72. IEEE, 2009. Google Scholar
  14. Marc Schlickling and Markus Pister. Semi-automatic derivation of timing models for WCET analysis. In ACM Sigplan Notices, volume 45, 4, pages 67-76. ACM, 2010. Google Scholar
  15. Rathijit Sen and YN Srikant. Executable analysis with circular linear progressions. Technical report, Technical Report IISc-CSA-TR-2007-3, Computer Science and Automation Indian …, 2007. Google Scholar
  16. Wei-Tsun Sun and Hugues Cassé. Dynamic branch resolution based on combined static analyses. In 16th International Workshop on Worst-Case Execution Time Analysis-WCET 2016. OASICs, Dagstuhl Publishing, 2016. Google Scholar
  17. TriCore™ TriCore™ V1.6 Microcontrollers User Manual (Volume 2). Google Scholar
  18. Johan Van Praet, Dirk Lanneer, Werner Geurts, and Gert Goossens. nML: A structural processor modeling language for retargetable compilation and ASIP design. In Processor Description Languages, pages 65-93. Elsevier, 2008. Google Scholar
  19. Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, et al. The worst-case execution-time problem—overview of methods and survey of tools. ACM Transactions on Embedded Computing Systems (TECS), 7(3):36, 2008. Google Scholar
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