Comparison of Implicit Path Enumeration and Model Checking Based WCET Analysis

Authors Benedikt Huber, Martin Schoeberl



PDF
Thumbnail PDF

File

OASIcs.WCET.2009.2281.pdf
  • Filesize: 221 kB
  • 12 pages

Document Identifiers

Author Details

Benedikt Huber
Martin Schoeberl

Cite AsGet BibTex

Benedikt Huber and Martin Schoeberl. Comparison of Implicit Path Enumeration and Model Checking Based WCET Analysis. In 9th International Workshop on Worst-Case Execution Time Analysis (WCET'09). Open Access Series in Informatics (OASIcs), Volume 10, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)
https://doi.org/10.4230/OASIcs.WCET.2009.2281

Abstract

In this paper, we present our new worst-case execution time (WCET) analysis tool for Java processors, supporting both implicit path enumeration (IPET) and model checking based execution time estimation. Even though model checking is significantly more expensive than IPET, it simplifies accurate modeling of pipelines and caches. Experimental results using the UPPAAL model checker indicate that model checking is fast enough for typical tasks in embedded applications, though large loop bounds may lead to long analysis times. To obtain a tool which is able to cope with larger applications, we recommend to use model checking for more important code fragments, and combine it with the IPET approach.
Keywords
  • WCET analysis
  • model checking
  • IPET
  • Java
  • JOP
  • UPPAAL

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
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