Se ha publicado una nueva tesis de razonamiento formalizado en Coq: Représentation coinductive des graphes.
Su autora es Celia Picard dirigida por Ralph Matthes.
La tesis se presentó el 15 de junio en la Universidad de Toulouse (Université Toulouse III Paul Sabatier).
Su resumen es
Contexte général
Ce travail s’inscrit à l’interface de l’Ingénierie Dirigée par les Modèles et de la théorie des types. Dans le contexte toulousain, fortement axé vers les systèmes embarqués et critiques, savoir certifier la représentation et la transformation des modèles est un enjeu majeur. La perspective visée ici est la transformation d’un modèle conforme à un métamodèle en un modèle conforme à un autre métamodèle en assurant certaines propriétés sur le modèle d’arrivée. Deux solutions sont possibles pour cela : vérifier les propriétés sur chaque modèle d’arrivée ou certifier que l’application de la transformation assure ces propriétés. Nous avons choisi cette seconde solution. Pour la certification, nous avons décidé dans un premier temps d’utiliser un prouveur interactif, le système Coq. La première étape consiste à représenter les métamodèles, la seconde à établir un langage permettant d’exprimer les propriétés à vérifier. Dans cette thèse, nous nous intéressons à la représentation et la manipulation de métamodèles sous forme de graphes.
La représentation des graphes
Nous avons décidé de représenter les graphes par des types coinductifs dont nous voulions explorer l’utilisation dans Coq. En effet, la représentation de la coindition dans les prouveurs basés sur la théorie des types est en progrès continuel. De plus, l’utilisation des types coinductifs permet de rendre succincte et élégante notre représentation des graphes et d’obtenir la navigabilité par construction. Nous avons dû contourner la condition de garde dont le but est d’assurer la validité des opérations effectuées sur les objets coinductifs. Son implantation dans Coq (compromis entre expressivité et maniabilité, résultat d’une longue évolution) est restrictive, et interdit parfois des définitions sémantiquement correctes. Une formalisation canonique des graphes dépasse ainsi l’expressivité directe de Coq. Nous avons donc proposé une solution respectant ces limitations, puis nous nous sommes intéressés à la définition d’une relation plus permissive sur les graphes. Celle-ci permet d’obtenir la même notion d’équivalence qu’avec une représentation classique (ensemble de nœuds/ensemble d’arêtes) tout en gardant les avantages de la coinduction. En effet, notre définition des graphes crée un ordre implicite (horizontal et vertical) entre les nœuds. Notre nouvelle relation permet de nous en affranchir. Nous montrons qu’elle est équivalente à une relation basée sur des observations finies des graphes. Ces résultats ont fait l’objet de publications et sont certifiés par des développements Coq. Toutefois, ces derniers ont été transcrits en langage mathématique et la lecture de cette thèse ne requiert pas de connaissance de Coq.
La formalización en Coq se encuentra aquí.