Document Open Access Logo

Formal Executable Models for Automatic Detection of Timing Anomalies

Authors Mihail Asavoae, Belgacem Ben Hedia, Mathieu Jan

PDF
Thumbnail PDF

File

OASIcs.WCET.2018.2.pdf
  • Filesize: 387 kB
  • 13 pages

Document Identifiers

Author Details

Mihail Asavoae
  • CEA LIST, Gif-sur-Yvette, France
Belgacem Ben Hedia
  • CEA LIST, Gif-sur-Yvette, France
Mathieu Jan
  • CEA LIST, Gif-sur-Yvette, France

Cite AsGet BibTex

Mihail Asavoae, Belgacem Ben Hedia, and Mathieu Jan. Formal Executable Models for Automatic Detection of Timing Anomalies. In 18th International Workshop on Worst-Case Execution Time Analysis (WCET 2018). Open Access Series in Informatics (OASIcs), Volume 63, pp. 2:1-2:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/OASIcs.WCET.2018.2

Abstract

A timing anomaly is a counterintuitive timing behavior in the sense that a local fast execution slows down an overall global execution. The presence of such behaviors is inconvenient for the WCET analysis which requires, via abstractions, a certain monotony property to compute safe bounds. In this paper we explore how to systematically execute a previously proposed formal definition of timing anomalies. We ground our work on formal designs of architecture models upon which we employ guided model checking techniques. Our goal is towards the automatic detection of timing anomalies in given computer architecture designs.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Real-time systems
  • Computer systems organization → Embedded systems
Keywords
  • timing anomalies
  • predictability
  • formal methods
  • model checking

Metrics

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

References

  1. J. Eisinger, I. Polian, B. Becker, A. Metzner, S. Thesing, and R. Wilhelm. Automatic identification of timing anomalies for cycle-accurate worst-case execution time analysis. In DDECS, pages 15-20, 2006. Google Scholar
  2. G. Gebhard. Timing anomalies reloaded. In WCET, pages 1-10, 2010. Google Scholar
  3. G. Gebhard. Static timing analysis tool validation in the presence of timing anomalies. PhD thesis, Saarland University, 2013. Google Scholar
  4. S. Hahn, M. Jacobs, and J. Reineke. Enabling compositionality for multicore timing analysis. In RTNS, pages 299-308, 2016. Google Scholar
  5. S. Hahn, J. Reineke, and R. Wilhelm. Towards compositionality in execution time analysis: Definition and challenges. SIGBED Rev., 12(1):28-36, 2015. Google Scholar
  6. J. Henry, M. Asavoae, D. Monniaux, and C. Maiza. How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. In LCTES, pages 43-52, 2014. Google Scholar
  7. R. Kirner, A. Kadlec, and P. Puschner. Precise worst-case execution time analysis for processors with timing anomalies. In ECRTS, pages 119-128, 2009. Google Scholar
  8. L. Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., 2002. Google Scholar
  9. M. Langenbach, S. Thesing, and R. Heckmann. Pipeline modeling for timing analysis. In SAS, pages 294-309, 2002. Google Scholar
  10. J. Larus. Whole program paths. In PLDI, pages 259-269, 1999. Google Scholar
  11. T. Lundqvist and P. Stenström. Timing anomalies in dynamically scheduled microprocessors. In RTSS, pages 12-21, 1999. Google Scholar
  12. S. Merz. On the logic of TLA+. Comp. and Artificial Intelligence, 22(3-4):351-379, 2003. Google Scholar
  13. J. Reineke and R. Sen. Sound and efficient WCET analysis in the presence of timing anomalies. In WCET, 2009. Google Scholar
  14. J. Reineke, B. Wachter, S. Thesing, R. Wilhelm, I. Polian, J. Eisinger, and B. Becker. A definition and classification of timing anomalies. In WCET, 2006. Google Scholar
  15. L. Thiele and R. Wilhelm. Design for timing predictability. Real-Time Systems, 28(2-3):157-177, 2004. Google Scholar
  16. I. Wenzel, R. Kirner, P. Puschner, and B. Rieder. Principles of timing anomalies in superscalar processors. In QSIC, pages 295-306, 2005. Google Scholar
  17. R. Wilhelm, D. Grund, J. Reineke, M. Schlickling, M. Pister, and C. Ferdinand. Memory hierarchies, pipelines, and buses for future architectures in time-critical embedded systems. IEEE Trans. on CAD of Integrated Circuits and Systems, 28(7):966-978, 2009. Google Scholar
  18. Y. Yu, P. Manolios, and L. Lamport. Model checking TLA+ specifications. In CHARME, pages 54-66, 1999. 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact