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