WUPPAAL: computation of worst-case execution-time for binary programs with UPPAAL

Franck Cassez*, Pablo Gonzalez de Aledo, Peter Gjøl Jensen

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review

4 Citations (Scopus)


We address the problem of computing the worst-case execution-time (WCET) of binary programs using a real-time model-checker. In our previous work, we introduced a fully automated and modular methodology to build a model (network of timed automata) that combined a binary program and the hardware to run the program on. Computing the WCET amounts to finding the longest path time-wise in this model, which can be done using a real-time model checker like Uppaal. In this work, we generalise the previous approach and we define a generic framework to support arbitrary binary language and hardware. We have implemented our new approach in an extended version of Uppaal, called Wuppaal. Experimental results using some standard benchmarks suite for WCET computation (from Mälardalen University) show that our technique is practical and promising.

Original languageEnglish
Title of host publicationModels, algorithms, logics and tools
Subtitle of host publicationEssays dedicated to Kim Guldstrand Larsen on the occasion of his 60th birthday
EditorsLuca Aceto, Giorgio Bacci, Giovanni Bacci, Anna Ingólfsdóttir, Axel Legay, Radu Mardare
Place of PublicationCham
PublisherSpringer, Springer Nature
Number of pages18
ISBN (Electronic)9783319631219
ISBN (Print)9783319631202
Publication statusPublished - 2017

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • Binary program
  • Control flow graph
  • Worst-case execution-time


Dive into the research topics of 'WUPPAAL: computation of worst-case execution-time for binary programs with UPPAAL'. Together they form a unique fingerprint.

Cite this