Software
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).
