Software
FLATA
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.
j-POST
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.
BIP
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.
IF
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.
IFx
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).
