Trustworthy Systems

Timing analysis of binary programs with UPPAAL

Authors

Franck Cassez and Jean-Luc Bechennec

NICTA

Abstract

We address the problem of computing accurate Worst-Case Execution Time (WCET) on pipelined architectures with caches. We propose a fully automatic and modular methodology based on program slicing and real-time model-checking. We have implemented our methodology and applied it to standard benchmarks. To further validate the approach, we also compare our results to the real execution times of the programs measured on a real board.

BibTeX Entry

  @inproceedings{Cassez_Bechennec_13,
    month            = jul,
    keywords         = {wcet, model-checking, timed automata},
    publisher        = {IEEE Computer Society},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/5929.pdf},
    booktitle        = {13th International Conference on Application of Concurrency to System Design (ACSD)},
    author           = {Cassez, Franck and Bechennec, Jean-Luc},
    year             = {2013},
    pages            = {41--50},
    address          = {Barcelona, Spain},
    title            = {Timing Analysis of Binary Programs with {UPPAAL}}
  }

Download