FIACRE
Models and Tools for Safety and Security Analysis
of Distributed Components
and their Composition
Welcome to the home page of the FIACRE project
Keywords
Distributed applications, Composition of components, Model extraction,
Temporal logic, Model-checking, Behavioural specification, Behavioral typing, Model-based verification, Compositional verification
Abstract
In forthcoming years, distributed component based programming will have a strong impact on software development methods.
In order for this approach to fully work, while component libraries become available, it is necessary to be able to compose existing components into more complex objects, and to guarantee that this composition will work correctly and fulfill its expected role.
Classical, static interface typing does not allow to reach this goal.
Gathering teams specialized in behavioural specifications of
components, languages and models for distributed, mobile, and
communicating application programming, and methods and tools for
compositional verification, the goal of FIACRE is to design methods and
tools for specification, model extraction, and verification of
distributed, hierarchical, and communicating components.
Our proposal is articulated around the following axes:
- Definition of languages to specify properties and component behaviours,
which must be adapted to verify distributed applications and allow an
easy translation into the low-level formalisms that are used for
verification, and into distributed application skeletons (for model
based code generation).
We shall also study the integration of behavioural typing within this language.
- Behavioural model extraction of distributed components, for which finite
state abstractions are necessary.
The challenge is to define semi-automated procedures that avoid user
interventions as far as possible.
- Verification (either using temporal logic formulas, behavioural equivalences, or behavioural typing) of the hierarchical compositions of components from their behavioural specifications.
This necessitates to fight against state explosion to verify large
systems, using in particular techniques such as partial orders or compositional
verification, or through the use of techniques dedicated to parameterized or
infinite systems.
Our proposal relies on serious approaches and software tools existing
in the participating teams, in particular the ProActive software component
library (INRIA/OASIS) distributed within ObjectWeb, the CADP verification
toolbox (INRIA/VASY), the TINA verification tool (FERIA/SVF), and the
behavioural typing approach (ENST/ILR).
We would like the collaboration to result in a software prototype
applicable to realistic applications.
Start : 1st sep. 2004
Duration : 3 years
Eric Madelaine
Last modified: Mon Jan 17 16:48:51 MET 2005