Distributed and Complex Systems Group : Homepage

:Vérimag Distributed and Complex Systems Group



FLATA is a tool for the reachability analysis of non-deterministic integer programs (also known as counter automata models). The tool takes as input a textual (ascii) description of the automaton, together with a specification of the final locations for which we test reachability. The input model is reduced (by applying a number of heuristics) to an equivalent (from the reachability point of view) smaller model. The latter can be analyzed by a built-in acceleration procedure, or it can be exported to other analysis tools, such as FAST or ARMC. The built-in analysis uses abstraction to reduce the reachability problem to a more general SMT problem, which is solved invoking Yices. Abstraction is however not needed if the model is flat, i.e. if the control structure has no nested loops.

->Link to the FLATA tool page


an integrated tool chain for property-oriented software testing from partial specifications.

This tool chain includes a test designer, a test generator, and a test execution engine. The test generation is based on an original approach which consists in deriving a set of communicating test processes obtained both from a requirement formula (expressed in a trace-based logic) and a behavioral specification of some specific parts of the software under test. The test execution engine is then able to coordinate the execution of these test processes against a distributed Java program. A typical application of j-POST is to check the correct deployment of security policies.

->Link to the j-POST tool page


a tool for program verification with singly linked list.

->Link to the L2CA tool page


a tool for incremental component-based construction and validation of real-time systems.

The aim is to develop theory, methods and tools for building real-time systems consisting of heterogeneous components. The focus is on the following challenging problems :

  • Develop a framework for the incremental composition of heterogeneous components. Three different sources of heterogeneity are considered related to interaction, execution and abstraction.
  • Develop results ensuring correctness-by-construction for essential system properties such as mutual exclusion, deadlock-freedom and progress in order to minimize a posteriori validation.
  • Provide automated support for component integration and generation of glue code meeting given requirements.

->Link to the BIP page


a tool environment for the verification of distributed systems.

IF is a tool environment for the verification of distributed systems consisting of a compiler for SDL (based on an API of ObjectGeode), static analysis tools, simulators, model-checkers and equivalence checkers based on the intermediate representation IF; this intermediate form is based on timed automatas with urgencies extended with data, and communicating either asynchronosly through buffers, synchronosly by rendez-vous or by shared variables.

->Link to the IF page


a simulation and verification environment for real time UML models derived from IF.

IFx is a simulation and verification environment for real time UML models, derived from IF. It contains a compiler of UML models (in XMI format) to IF, a simulation GUI targeted at UML designers and an extended version of IF (with observers and other features).

->Link to the IFx page


a tool verifying secrecy properties of unbounded security protocols.

->Link to the Hermes page

CADP (Caesar/Aldebaran Distribution Package)

a toolbox devoted to the validation of Lotos programs - developed together with the team Vasy of Inria Rhône-Alpes.

->Link to the CADP page