Outils

Lustre V6
Lustre V6 is the last version of the academic Lustre compiler, featuring an ada-like package mechanism, structured data-types (enums, structures), array iterators, and static recursion.

The Lustre V6 toolbox (lus2lic, lurette, rdbg)

Multi-core interference Analysis
A timing analysis tool for multi-core : From a description of data-flow application and initial schedule and mapping, it produces an updated schedule (release dates) that takes into account the inter-task interference. The focus is on the interference due to shared bus.

PADEC A Framework for Certified Self-Stabilization
PADEC is a framework to build certified proofs of self-stabilizing algorithms using the Coq proof assistant. The framework includes the definition of the computational model, lemmas for common proof patterns and case studies. A constant purpose was to convince the designers that what we formally prove using PADEC is what they expect by using definitions that are (syntactically) as close as possible to their usual definitions.

RDBG a Reactive programs DeBuGger
rdbg is now part of the Lustre V6 toolbox (lus2lic, lurette, rdbg)

SASA a SimulAtor of Self-stabilizing Algorithms
SASA is a Self-stabilizing Algorithms SimulAtor, based on the so-called Atomic State model (ASM) introduced by Dijkstra in its seminal article on Self-stabilizing distributed algorithms.