Formalisation et vérification d’un UIDL formel bigraphique dans Coq

Contexte général

Avec le développement des dispositifs d’interaction, en particulier tactiles, les systèmes interactifs se multiplient. Les systèmes critiques n’échappent pas à cette règle. Ainsi, les cockpits, autrefois tangibles et mécaniques, embarquent maintenant des tablettes tactiles, des écrans numériques et autres dispositifs interactifs. Pour accompagner cette multiplication des systèmes interactifs critiques, il est nécessaire que les langages supportant le développement de ces systèmes d’une part soient dédié à la création de tels systèmes et d’autre part apportent des garanties sur les systèmes développés, notamment dans leur processus de compilation. Ce n’est pas le cas actuellement.

Contexte scientifique

Les UIDLs sont des langages dédiés au développement de systèmes interactifs. Leur utilisation pour le développement de systèmes critiques est de plus en plus répandue, ainsi il est nécessaire de leur donner un fondement théorique solide afin de pouvoir apporter des garanties sur leur compilation et leur exécution.
Dans de précédents travaux, nous avons montré que la théorie des bigraphes, définie par Robin Milner dans les années 2000, était particulièrement adaptée pour exprimer la sémantique des UIDLs. Nous avons également défini un UIDL minimal formel à l’aide des bigraphes. Un bigraphe est un graphe qui permet de représenter à la fois des notions de localité (d’imbrication de composants les uns dans les autres) et de lien causaux (permettant de décrire des réactions en chaîne) au travers de deux sous-graphes. On peut ensuite décrire des évolutions de ces bigraphes (selon des évènements par exemple) via des règles de réaction qui décrivent comment transformer une sous-partie d’un bigraphe si certaines conditions sont respectées. On appelle système réactif bigraphique un bigraphe et les règles de réaction qui décrivent sa dynamique.

Pour pouvoir aller plus loin et raisonner formellement sur cet UIDL minimal (à la fois pour apporter des garanties sur la compilation et vérifier des propriétés), il est nécessaire de formaliser la théorie des bigraphes dans un assistant de preuve. Pour pouvoir ensuite nous insérer dans des écosystèmes tels que CompCert (un compilateur vérifié pour le langage C), nous avons choisi d’utiliser l’assistant de preuve Coq , et avons formalisé la partie structurelle (statique) des bigraphes et montré que notre formalisation est correcte.
 

Travaux visés

Le travail de cette thèse consiste à compléter l’implémentation des bigraphes dans Coq en
ajoutant les aspects dynamiques (les règles de réaction) puis à instancier notre formalisation
pour définir notre UIDL formel. Ce travail sera divisé en 4 parties :
1. Compléter l’implémentation des bigraphes dans Coq pour permettre le pattern matching
2. Implémenter la définition des règles de réaction pour permettre la définition d’un système
réactif bigraphique à l’aide du pattern matching
3. Instancier cette formalisation pour définir notre UIDL formel dans Coq
4. Prouver sur ce modèle formel les propriétés sur les UIDLs formels
 

Aspect novateur

La théorie des bigraphes a été développée par Milner au début des années 2000. C’est donc une
théorie récente et seulement partiellement explorée. Elle est destinée à la description de systèmes
réactifs mais n’a pas été utilisée pour la définition de la sémantique de langages réactifs ni pour
leur compilation. Elle a néanmoins été utilisée pour définir la sémantique du langage Kappa,
un langage à base de règles pour la modélisation des réseaux d’interaction. Bien qu’elle soit
utilisée pour faire de la simulation et du model checking, elle n’a pas été encore définie dans un
assistant de preuve, ni utilisée pour la démonstration de propriétés. Par ailleurs, la formalisation
et la validation de composants interactifs et graphiques est un défi à part entière, peu ou pas
traité dans la littérature. En général, ces composants sont validés de façon empirique par des
tests utilisateurs et des recettes, qui sont coûteuses en temps et non exhaustives.
 

Aspects organisationnels

• La thèse débutera à l’automne 2025 et pourra être précédée d’un stage de M2.
• La thèse se déroulera entre l’ISAE-Supaero et l’ENAC, à Toulouse. Le contrat sera signé à l'ENAC qui sera également l'établissement d'inscription. La doctorante ou le doctorant aura un bureau dans chacune des deux institutions.
• Il est possible d’effectuer de l’enseignement durant la thèse.
• Nous travaillons en collaboration avec l’Université de Glasgow, spécialistes des bigraphes. Un échange de quelques semaines avec cette université durant la thèse est envisageable.
• Le salaire se situe autour de 2600€ brut mensuel, hors enseignement.
• En plus de ses congés annuels et RTT, le ou la doctorant.e bénéficiera d'une demie journée de congé supplémentaire par semaine

Le doctorat se déroulera entre les équipes CASC (ISAE-Supaero - https://www.isae-supaero.fr/fr/recherche/departements/ingenierie-systemes-complexes/groupe-ingenierie-pour-les-systemes-critiques-460) et LII (ENAC - https://lii.enac.fr/). Ces équipes sont situées dans deux écoles majeures de la scène aéronautique européenne.

• Bac+5 ou équivalent en informatique
• Notions en méthodes formelles, idéalement en Coq, ou au moins une forte appétence pour
  la théorie et la preuve de programme
• Notions en compilation
• Bon niveau d’anglais (lu, écrit, parlé)