PoC/Demo: Improving WCET Evaluation using Linear Relation Analysis


This proof-of-concept demo illustrates the use of a Abstract Interpretation tool (pagai) for finding infeasible paths in C programs. The goal is to enhance the Worst Case Execution Time (WCET) estimation, using the otawa framework for timing analysis.

It has been developed during the W-SEPT project.


Improving WCET Evaluation using Linear Relation Analysis. Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Jahier, Erwan and Halbwachs, Nicolas and Carrier, Fabienne and Asavoae, Mihail and Boutonnet, Rémy (in Leibniz Transactions on Embedded Systems, 2019)


Dowload cnt-demo-vm.zip.

This proof-of-concept/demo is distributed as a virtual machine. To run it you must have VirtualBox installed on x86_64 machine running a 64 bits OS. The VM has been tested on Windows 10, Debian (buster), Ubuntu (Bionic Beaver), and VirtualBox 6.1 and 6.2.


  • Install the directory in your default VM folder (generally $home/VirtualBox VMs).
  • Run VirtualBox, select Machine/Add, browse to the corresponding .vbox file
  • Run the demo
  • Within the VM, follow the instructions in the README file(s)


  • Note that these demos are command-line, so you should be familiar with basic Linux commands (vi, more, make etc.)
  • If the provided .vbox does not work (e.g. older version of VirtualBox), you can try to create your own virtual machine via Machine/New:
    • select Type: Linux, Version: Other Linux (64 bits)
    • 1024 MB RAM (at least 512 MB)
    • Use an existing virtual hard disk file: browse to the-demo.vdi
    • It’s probably possible to run the demo with another virtualization tool by re-encoding the .vdi virtual disk into another format (not tested).
    • If the VM hangs on starting, with an image displaying “Tiny Core” try “Machine/Reset