Proofs of Concept and demos

This folder lists tools developed to illustrate academic research. They are strongly system dependent, and are thus distributed within ad hoc virtual machines.

PoC/Demo: Improving WCET Evaluation using Linear Relation Analysis

Purpose 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. Reference: 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)

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)