Home > Teams > Synchrone > Tools > Tools
Tools
Tools
- aadl2sync
An AADL to synchronous programs translator
- aadl4ocaml
an ocaml library for parsing AADL code.
- Argos and Larissa
Argos is an automaton language, similar to StateCharts, but with synchronous semantics.
- Aspic Accelerated Symbolic Polyhedral Invariant Computation
This software is based on Linear Relation Analysis, and combines classic LRA (with widening) and acceleration techniques.
- BDDC v2
A Binary Decision Diagrams library, initially written for the Lustre compiler in the early 90s.
- 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.
- LIBTLMPWT Model Power-Consumption and Temperature in SystemC/TLM
Library for power consumption and thermal modeling.
- Lurette An automatic testing tool for reactive systems.
Lurette is now part of the Lustre V6 toolbox (lus2lic, lurette, rdbg)
- Lustre V4 Toolbox
The Lustre Toolbox includes Lustre V4 and the model-checker Lesar.
- 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.
- Lutin
A (target) language for describing and simulating stochastic reactive systems.
Lutin is now part of the Lustre V6 toolbox (lus2lic, lurette, rdbg)
- 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).
- RDBG a Reactive programs DeBuGger
rdbg is now part of the Lustre V6 toolbox (lus2lic, lurette, rdbg)
- Reglo
A compiler which translates regular expressions into either a set of language equations, or into a Lustre program.
- sc-during
Library for parallel programming on top of SystemC
- 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
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
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.
