An AADL to synchronous programs translator
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.
- BIP Behavior Interaction Priority
The BIP toolset includes translators from various programming modes into BIP, source-to-source transformers as well as a compiler for generating code executable by a dedicated engine.
- BIP System Designer
The BIP System Designer is the complete tool-set to obtain a system model of a mixed software/hardware system, that can be simulated, analyzed (verification of functional + extra-functional properties), and used to generate the software stack (application software + hardware dependent software) for a target platform.
The tools are classified as follows:
Translation of application software model into application model in BIP. The translator from DOL to BIP is here.
- D-Finder a compositional deadlock detection and verification tool for BIP models
is a prototype tool for reachability analysis of continuous and hybrid systems
FLATA is a tool for the analysis of non-deterministic linear integer programs (also known as counter automata).
FLATA-C is static-analysis front-end, implemented as a FRAMA-C plugin, that aims at extracting Numerical Transition System models from C programs with low-level pointer updates such as e.g.: allocation, deletion, pointer arithmetic, etc. The generated NTS models can be used with off-the-shelf verifiers such as FLATA or ELDARICA.
We target the following types of errors in the C code:
null or dangling pointer dereferencing unaligned memory accesses memory leaks double free out-of-bound (...)
- 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.
- InVeSt Invariants Verification System
InVeSt is a tool for verification of invariance properties of infinite state systems.
Kronos is a tool for model-checking of timed automata against specifications
expressed using the real-time temporal logic TCTL.
- L2CA a tool for the analysis of pointer programs
Lists to Counter Automata: a tool for the analysis of pointer programs
- 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 an Automatic Test Generator for Reactive Programs.
- 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.
A (target) language for describing and simulating stochastic reactive systems.
A quantifier elimination tool
- Multicore Code Generation for Time-critical Applications
A diagram of the tool chain for code generation is shown in the figure above. The top-part represents a high-level design, serving as input to the tool chain. Currently we support high level designs from the DOL Critical framework. The framework should provide the model of the application (task graph) and the model of deployment (mapping). The application model includes both the task communication structure (here: the DOL-Cr XML) and the task functions (here: the C files). The mapping file (...)
- New BIP tools
The new version of the BIP compiler and engines is available now. Notice that we slightly modified the BIP language (its syntax and its semantics) with respect to the old versions the tools that are still available here.
contact: Jacques Combaz, developer: Anakreontas Mentis, former developer: Marc Poulhiès
The BIP tools provided here consist of a compiler for generating code from BIP sources, and an execution engine used as a scheduler for executing the generated code. We (...)
This library provides an algorithmic infrastructure for reachability computation of non-linear dynamical systems.
is an on-the-fly verification tool for timed automata based
on an integration of the DBM library of Kronos into
- Pagai a static analyzer
Pagai is a static analyzer based on the LLVM framework.
is a tool for reachability analysis of continuous and hybrid systems based on Linear Hybrid Automata.
- 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.
SystemC front-end based on LLVM, and back-ends to generate code like Promela (input language for SPIN).
- RDBG a Reactive programs DeBuGger
RDBG a programmable debugger that targets reactive programs for which a rdbg-plugin exists. Currently two plugins exist : one for Lustre, and one for Lutin (nb: both are synchronous programming languages).
A compiler which translates regular expressions into either a set of language equations, or into a Lustre program.
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.
- SMI Symbolic Model Interface
The Symbolic Model Interface (SMI) is a library which provides for the efficient construction and manipulation of symbolic representations for finite state systems, in particular for communication protocols.
- 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.
- TGV Test Generation with Verification technology
TGV (Test Generation with Verification technology) is a tool for the generation of conformance test suites for protocols. It is the result of a collaboration of the project Pampa of the Irisa institute with the projet Spectre/INRIA of the Verimag research center.