This Toolbox gathers currently maiontainde tool around Lustre and the synchronous approach, in particular the The Lustre V6 compler and the Lutin/Lurette testing tool.
It is available on the Verimag website.
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)
Yacc2latex generates human-readable EBNF grammars from yacc files. Output format is in Latex and fairly customizable.
Distribution yacc2latex is available under LGLP licence (dowload here).
Goal As a language designer, I often faced the problem of writing and maintaining a reference (readable) grammar of my language. This is particularly annoying since the reference grammar actually exists as a yacc (or ocamlyacc) file, so why not use a “compiler” that will derived automaticaly the reference grammar from the yacc file ?
Reglo compile regular expressions into logical circuits (in Lustre).
User manual
BDDC is a basic logical calculator.
User manual
