Méthodes catégoriques et logiques en transformations de modèles – CLIMT

Il existe de nombreuses manières d'aborder le problème de la qualité
des logiciels. Le spectre de ces techniques s'étend des obligations de
preuves, des conceptions d'architecture, des langages de
spécifications, des langages de programmation jusqu'au test et à la
vérification de programmes. Ces méthodes sont souvent spécifiques à
un paradigme de programmation donné. La programmation déclarative à
base de règles est une des approches abstraites parmi les plus
prometteuses pour l'amélioration de la productivité et de la qualité
du logiciel.

La programmation basée sur des règles permet en général
une meilleure lisibilité, écriture et maintenance du logiciel. Quand les
règles opèrent sur des objets représentés par des arbres (ou des
chaînes de caractères), beaucoup de techniques de vérification de
programmes ont été proposées dans la littérature renforçant
considérablement la qualité du logiciel. Cependant de nombreux
problèmes pratiques ne peuvent être encodés facilement sous
forme d'arbres. Ces problèmes nécessitent l'utilisation de structures
plus élaborées comme les graphes. Les graphes sont des objets
mathématiques très communs, visuellement parlant et intuitifs. Ils
constituent une approche naturelle de la modélisation qui est utilisée
dans de nombreux domaines scientifiques comme l'informatique, les
sciences du vivant, l'économie ou la sociologie.

L'objectif du projet CLIMT consiste en le développement de nouveaux
formalismes de haut niveau afin de donner des bases théoriques, facilitant
la vérification de programmes basés sur des règles opérant sur des structures
de données complexes modélisées par des graphes. A cette fin nous
allons organiser notre recherche selon les trois axes suivants~:

(i)Le premier consiste en l'étude de nouvelles classes
de système de réécriture de graphes avec une attention particulière
portée sur de nouveaux traits comme le clonage ou l'utilisation d'attributs
inductifs.

(ii)Le second axe de recherche consiste en la définition de
nouvelles logiques et techniques de preuves pour exprimer et
réaliser de manière semi automatique des preuves de correction et de
propriétés des systèmes de réécriture considérés.

(iii) Dans le troisième axe, nous étudierons des techniques de
preuves dont le but est d'améliorer l'espace de recherche des
systèmes d'aide à la preuve des systèmes de réécriture de
graphes. Ceci se fera par exemple en faisant appel à des procédures
spécialisées (SAT ou SMT) ou en utilisant des techniques de
détection de symétrie afin d'éviter les redondances.


Ce projet sera une opportunité de réunir des expertises
complémentaires dans les domaines de la transformation de graphes,
des systèmes de preuve automatique, de la logique pour proposer de
nouvelles méthodes formelles, des techniques efficaces et des outils
spécifiques pour le développement et la certification de programmes
basés sur des règles et opérant sur des graphes.