Nos partenaires

CNRS

Rechercher





Accueil du site > Français > Thèmes de recherche > Thème 7 - Sûreté de développement du logiciel > Equipe MACAO > Evénements

Soutenance de thèse de Bertrand Boisvert - 30 septembre 2013 - 10h30

Catégories, $\lambda$-calcul typé, et Preuves pour la Transformation de Graphes Attribués

Les graphes sont des entités abstraites composées de noeuds reliés par des arcs. Les graphes attribués sont des graphes avec des informations supplémentaires ``attachées’’ aux noeuds et/ou aux arcs.

Les graphes attribués sont des outils de plus en plus utilisés pour modéliser toute sorte de systèmes, dans de nombreux domaines scientifiques. En particulier, dans le domaine du génie logiciel, les graphes attribués permettent de modéliser, de concevoir, et d’étudier les logiciels. En effet de nombreux langages de modélisation et de formalisation utilisent des graphes attribués comme représentation de base (automates temporisés, diagrammes de classes UML, réseaux de Petri, etc).

En informatique comme dans d’autres domaines, l’aspect dynamique est très important. Pour représenter l’évolution des systèmes modélisés ou pour utiliser les modèles dans un but génératif, il est nécessaire de réaliser des transformations de graphes attribués. Il faut alors réaliser à la fois une transformation de la structure du graphe, et des calculs sur les attributs.

De nombreuses approches de transformation de graphes existent. Peu d’approches considèrent le problème des attributs et des calculs sur ces attributs. Les approches qui le font (Double Pushout et Single Pushout) rencontrent des difficultés quand à la puissance de calcul et à l’implémentation de la théorie. Certaines de ces difficultés viennent de choix techniques, et d’autres sont intrinsèquement liées au fait de considérer des attributs sur une structure de graphe.

Cette thèse a pour but d’étudier les problèmes posés par les attributs dans les transformations de graphes attribués, et de proposer des solutions pour traiter les problèmes rencontrés par les autres approches. Dans le cadre de ces travaux, deux approches de transformation de graphes attribués sont proposées. Ces deux approches sont basées sur l’approche Single Pushout, dans le cadre de la théorie des catégories. Dans la première approche, les attributs et les calculs sont décrits à l’aide du lambda-calcul avec les types inductifs. Dans la seconde les attributs sont décrits à l’aide de séquents logiques, et les calculs sont décrits par des preuves. Ces choix permettent d’avoir un meilleur pouvoir expressif des attributs, et une plus grande puissance de calcul. Une analyse de ces approches, et une comparaison avec les approches existantes dans ce domaine a permis de tirer de nombreux enseignements, et fournit des perspectives pour le développement de meilleurs systèmes de transformation de graphes attribués.