Tools

Main

The Lustre V4 Toolbox [Binary distribution, basic maintenance]
The Lustre Toolbox includes Lustre V4 and the model-checker Lesar.
The Synchrone Reactive Toolbox [Binary distribution, active maintenance]
This Toolbox consists of development tools targeting the design of reactive programs (typically, for critical embedded systems). It features the Lustre V6 language compiler and interpreter, the Lutin reactive system environment modeling language interpreter, the Lurette automated testing tool, the Lesar model-checker, the RDBG (Reactive Programs) debugger, and the gnuplot-rif and sim2chro data visualizers.

BDDC v2 [Binary distribution, basic maintenance]
A command-line logical calculor, based on the Binary Decision Diagrams library of the Lustre compiler.
Lutin [Open-source distribution, active maintenance]
A (target) language for describing and simulating stochastic reactive systems.

Lutin is now part of the Lustre V6 toolbox (lus2lic, lurette, rdbg)
Multi-core interference Analysis [Binary distribution, beta, basic maintenance]
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.
Reglo [Binary distribution, basic maintenance]
A compiler which translates regular expressions into either a set of language equations, or into a Lustre program.

Initially developped at Verimag, the tools and prototypes below are now distributed elsewhere.

Aspic Accelerated Symbolic Polyhedral Invariant Computation
This software is based on Linear Relation Analysis, and combines classic LRA (with widening) and acceleration techniques.
LIBTLMPWT Model Power-Consumption and Temperature in SystemC/TLM
Library for power consumption and thermal modeling.
Pinapa A front-end for SystemC/TLM
Pinapa is a front-end for SystemC/TLM, that allows to combine the information on the architecture of a TLM platform, with the syntax trees of the threads.
PinaVM
SystemC front-end based on LLVM, and back-ends to generate code like Promela (input language for SPIN).
sc-during
Library for parallel programming on top of SystemC

The tools below are prototypes or tools that are not active anymore.

aadl2sync [Binary distribution, pre-alpha, no maintenance]
An AADL to synchronous programs translator
aadl4ocaml [Open-source distribution, pre-alpha, no maintenance]
an ocaml library for parsing AADL code.
Argos and Larissa
Argos is an automaton language, similar to StateCharts, but with synchronous semantics.
IF Intermediate Format and Verification Tool set
The IF Intermediate Representation based on extending communicating timed automata has been defined for being able to offer a powerful toolset offering simulation, analysis and verification facilities for different modelling languages for distributed real-time systems.
SCRV Runtime verification for SystemC/TLM designs
SCRV allows to cover the non-determinism of the scheduling choices, when executing a SystemC/TLM model with the SystemC engine.
SR3 : Secure Resilient and Reputation-based Routing [Binary distribution, beta, no maintenance]
SR3 is a many-to-one routing protocol, designed for wireless sensor networks, which is both secure and resilient. It is a reinforced random walk that is partially determinized using a reputation mechanism.
ss2lus Simulink/Stateflow to Lustre [Binary distribution, beta, no maintenance]
The main objective of this project is to allow the translation of Simulink/Stateflow (trademarks of The Mathworks Inc.) into the synchronous programming language Lustre allowing its associated compilers, model-checkers and abtract interpretation tools to be applied to Simulink designs.