A Formal Framework for Precise Parametric WCET Formulas

Authors Benedikt Huber, Daniel Prokesch, Peter Puschner

Thumbnail PDF


  • Filesize: 0.5 MB
  • 12 pages

Document Identifiers

Author Details

Benedikt Huber
Daniel Prokesch
Peter Puschner

Cite AsGet BibTex

Benedikt Huber, Daniel Prokesch, and Peter Puschner. A Formal Framework for Precise Parametric WCET Formulas. In 12th International Workshop on Worst-Case Execution Time Analysis. Open Access Series in Informatics (OASIcs), Volume 23, pp. 91-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


Parametric worst-case execution time (WCET) formulas are a valuable tool to estimate the impact of input data properties on the WCET at design time, or to guide scheduling decisions at runtime. Previous approaches to parametric WCET analysis either provide only informal ad-hoc solutions or tend to be rather pessimistic, as they do not take flow constraints other than simple loop bounds into account. We develop a formal framework around path- and frequency expressions, which allow us to reason about execution frequencies of program parts. Starting from a reducible control flow graph and a set of (parametric) constraints, we show how to obtain frequency expressions and refine them by means of sound approximations, which account for more sophisticated flow constraints. Finally, we obtain closed-form parametric WCET formulas by means of partial evaluation. We developed a prototype, implementing our solution to parametric WCET analysis, and compared existing approaches within our setting. As our framework supports fine-grained transformations to improve the precision of parametric formulas, it allows to focus on important flow relations in order to avoid intractably large formulas.
  • Worst-case execution time analysis
  • parametric WCET analysis
  • path expressions
  • frequency expressions
  • algebraic framework


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail