Skip to main content


Timing analysis of binary programs with UPPAAL


Franck Cassez and Jean-Luc Bechennec



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

    publisher        = {IEEE Computer Society},
    author           = {Cassez, Franck and Bechennec, Jean-Luc},
    month            = jul,
    year             = {2013},
    keywords         = {wcet, model-checking, timed automata},
    title            = {Timing Analysis of Binary Programs with {UPPAAL}},
    booktitle        = {13th International Conference on Application of Concurrency to System Design (ACSD)},
    pages            = {41--50},
    address          = {Barcelona, Spain}


Served by Apache on Linux on seL4.