PoC/Demo: Timing Analysis Enhancement for Synchronous Program
Purpose
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.
Reference:
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)
Download/Install
Binaries for Linux64
Installation
- Download and unzip
- In a terminal, goto the directory, source the ‘setenv’ file
- Follow the README instructions
Virtual machine
For those that do not have a Linux pc, the 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.
Installation
- 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)
Troubleshooting
- 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