PoC/Demo: Timing Analysis Enhancement for Synchronous Program


This proof-of-concept demo illustrates the use of a model checker (lesar) for finding infeasible paths in a synchronous code (written in lustre). 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.


Timing analysis enhancement for synchronous program. Raymond, Pascal and Maiza, Claire and Parent-Vigouroux, Catherine and Carrier, Fabienne and Asavoae, Mihail (in Real-Time Systems, 2015)


Dowload w7-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