Objectifs

Dans le domaine de l’aide au développement de logiciel, les recherches visent à réduire les coûts et les délais de validation de logiciels critiques, par l’utilisation de méthodes formelles.

Trois axes sont explorés :

• La théorie des types, appliquée en particulier aux langages de spécification, au développement de preuves, et à la validation par preuve et vérification.
• L’aide au développement de systèmes réactifs, composites ou concurrents, répartis et mobiles. Les recherches portent sur les méthodes de développement, les langages dédiés, les systèmes hybrides exploitant des composants réactifs synchrones ou asynchrones. Les outils associés procèdent par analyse statique, par vérification de modèles ou par preuve. Ils peuvent traiter aussi bien des modèles abstraits que du code exécutable. Les systèmes embarqués et les grilles constituent pour cet axe des domaines d’application fédérateurs. Cet axe s’intéresse également à la coordination dans les systèmes d’information coopératifs, constitués d’agents plus ou moins autonomes partageant des connaissances.
• Le cycle de vie et les méta-modèles concernent les phases d’analyse et de conception. Les travaux portent sur les étapes de modélisation selon un formalisme à quatre niveaux : données, modèles, méta-modèles et méta-méta-modèles, où chaque niveau décrit le précédent. Plus généralement, cet axe explore la problématique de l’ingénierie des modèles, notamment la transformation, la vérification de cohérence et la méthodologie de construction.

Le thème participe à diverses actions nationales et régionales :

• RNTL : composants temps réel
• ACI Sécurité Informatique : composition et raffinement de systèmes sûrs, fiabilité de composants temps réel, politiques de disponibilité
• ACI GRID : architecture méta-donnée, moteur d’expertise et exécution sur grille
• TOPCASED : projet du pôle de compétitivité aéronautique, espace et systèmes

Ce thème diffuse également des logiciels libres :

• SYROCO : compilateur d’objets coopératifs
• GENSYS : générateur de compilateurs
• JAVACT : intergiciel pour agents mobiles adaptables
• NEPTUNE : UML : vérification, transformation
• FMONA : vérification de modèles

 Revenir à la rubrique Thème 7 - Sûreté de développement du logiciel