FIACRE
Fiabilité des Assemblages de Composants Répartis:
Modèles et Outils pour l'analyse d epropriétés de sécurité et de sureté
Bienvenue sur les pages du projet FIACRE
Mots-clés
Applications réparties, assemblage de composants, extraction de modèles,
logique
temporelle, model checking, spécification comportementale, typage
comportemental, vérification basée sur les modèles, vérification
compositionnelle.
Description
La programmation à base de composants distribués va avoir dans les
années qui viennent un impact important sur les méthodes de
développement de logiciels. Pour que cette approche fonctionne
pleinement, à mesure que des bibliothèques de composants deviennent
disponibles, il est indispensable de pouvoir assembler des composants
existants en des objets plus complexes, et de garantir que cet
assemblage fonctionnera correctement et remplira le rôle que l'on en
attend. Le typage classique, statique, des interfaces est notoirement
insuffisant pour atteindre ce but.
Réunissant des équipes spécialistes des spécifications
comportementales de composants, des langages et modèles pour la
programmation d'applications réparties, mobiles, communicantes, et des
méthodes et outils pour la vérification compositionnelle, l'objectif
de FIACRE est de concevoir des méthodes et des outils pour la
spécification, l'extraction de modèles et la vérification de
composants répartis, hiérarchiques et communicants.
Notre proposition s'articule autour des axes suivants :
- La définition de langages pour spécifier des propriétés et
le comportement des composants, qui doit être adapté pour
vérifier des applications distribuées et permettre une
traduction aisée vers les formalismes de bas niveau qui
sont utilisés pour la vérification, et la génération de
code. Nous étudierons également l'intégration du typage
comportemental à ce langage.
- L'extraction de modèles comportementaux pour les composants
répartis, pour laquelle des abstractions finies sont
nécessaires. Le défi consiste à définir des procédures
semi-automatiques qui permettent de limiter l'intervention
humaine au maximum.
- La vérification (par formules de logique temporelle, par
équivalence de comportements, ou par typage comportemental)
des assemblages hiérarchiques à partir des spécifications
comportementales des composants. Ceci nécessite de s'attaquer
au problème de l'explosion d'états des modèles afin de
vérifier des systèmes de grande taille, notamment à l'aide de
techniques telles que les ordres partiels ou la vérification
compositionnelle, ou à l'aide de techniques de vérification
de systèmes paramétrés.
Notre proposition s'appuie sur un certain nombre d'approches et
d'outils logiciels sérieux existants dans les équipes participantes,
en particulier la bibliothèque de composants ProActive (OASIS)
distribuée au sein d'ObjectWeb, la boîte à outils de vérification CADP
(VASY), l'outil de vérification TINA (SVF), et l'approche de typage
comportemental (ENST).
Nous souhaitons que la collaboration débouche
sur un prototype logiciel visant des applications réalistes.
Démarrage : 1er sep. 2004
Durée : 3 ans
Eric Madelaine
Last modified: Mon Jan 17 15:22:51 MET 2005