Langues : English français
Accueil > Manifestations > Thèses et HDR > HDR > HDR Christian Attiogbé

HDR Christian Attiogbé

Résumé

Nous présentons un ensemble de travaux sur l’intégration de méthodes
formelles et l’analyse multifacette de systèmes logiciels.

Le cadre général des travaux est celui des approches formelles pour la
construction de logiciels corrects.

Partant de l’idée que les différentes facettes d’un système doivent être étudiées et développées avec les formalismes et outils appropriés, tout en assurant les propriétés globales du système, nous avons exploré, suite à d’autres chercheurs, des pistes pour l’intégration de méthodes formelles utilisées pour spécifier, analyser ou développer des parties des systèmes. Dans cette optique, non seulement l’intégration des méthodes de spécifications formelles est considérée mais aussi celle des spécifications elles mêmes.

La nécessité de l’intégration est relative au besoin de l’interaction
entre différentes parties d’un même système ou bien à l’appréhension
globale des propriétés du système.

Nous explicitons les principaux problèmes de l’intégration de méthodes
formelles : l’hétérogénéité syntaxique, l’hétérogénétité sémantique et
la variété des systèmes logiques de raisonnement.

Nous proposons alors la notion de compatibilité relative à ces trois
niveaux pour effectuer l’intégration de méthodes. L’idée principale est
celle de l’interopérabilité sur une base sémantique (base d’intégration)
sans laquelle aucun raisonnement n’est possible entre des parties
assemblées d’un système. Les raisonnements formels sont alors effectués par plongement (shallow/deep embedding) des spécifications dans des logiques appropriées. Nous avons mis en évidence des schémas d’intégration type.

Ce premier cadre est généralisé avec la considération des domaines de compatibilité plus larges que les bases d’intégration, et qui permettent de s’affranchir des langages et de travailler au niveau des paradigmes sous-jacents aux langages ; on obtient ainsi un cadre pour une intégration générique.
Un tel cadre générique est le fondement pour la génération systématique d’environnements de spécification/développement à partir des paradigmes extraits des cahiers de charges. La nature des systèmes à développer guide alors non seulement le choix des méthodes/langages/outils de leur développement mais aussi l’élaboration (sur mesure) de l’environnement de développement approprié.

Nous avons montré comment les formalismes intégrés existants tels que
LOTOS, CSP-B, Circus rentrent dans le cadre des schémas d’intégration
type et nous avons mis en oeuvre cette approche pour de nouvelles
intégrations par exemple entre B et les réseaux de Pétri.

Dans une deuxième partie des travaux présentés, nous exposons des
extensions proposées autour de la méthode formelle B, notamment la composition parallèle asynchrone de systèmes abstraits B à la manière de la composition parallèle dans les algèbres de processus. Dans la version de composition asynchrone, nous considérons l’interaction sur la base des variables partagées.
Notre proposition permet de combiner dans un même projet de développement formel la démarche descendante de la méthode B avec une approche ascendante.

Nous présentons ensuite une méthode de construction systématique de
spécifications B pour des systèmes multi-processus à architecture ynamique.
Des système-types sont définis avec des contraintes de comportements
explicites (ordonnancement des événements) puis combinés pour interagir avec d’autres système-types (en partageant des événements).
Ces travaux généralisent les précédents sur la composition de systèmes
abstraits en définissant un opérateur de fusion de sous-systèmes qui est plus général que les opérateurs de composition parallèle.

Une troisième partie des travaux est consacrée à l’analyse multifacette de systèmes ; notre proposition consiste à assurer la compatibilité des
analyses des différentes facettes en partant non pas de modèles
indépendants mais de modèles spécifiques dérivés à partir d’un modèle de référence qui permet d’assurer la cohésion globale de l’analyse. Cette approche est poursuivie par des expérimentations sur la combinaison de prouveurs et d’évaluateurs de modèles (model-checkers).

D’autres voies sont explorées pour l’analyse multifacette :
élaboration d’une algèbre de spécifications multiparadigmes, ou différents aspects, relatifs aux facettes envisagées, peuvent être introduits dans une même unité de spécification. Les unités de spécification sont ensuite composées à l’aide des opérateurs de l’algèbre. Le lien est fait entre cette approche et celle de l’intégration de méthodes par plongement dans des logiques formelles.
Une plateforme expérimentale est développée conjointement à ces travaux et relie les deux approches : elle permettra à terme de traduire,
moyennant la compatibilité sémantique, différents formalismes d’entrées
dans des formalismes cibles en passant par un modèle formel de référence qui lui même est une spécification multiparadigme.

Dernière modification : mercredi 27 juillet 2011