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)
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)
