Nos offres
Retour aux offres

Doctorante / Doctorant Méthodes formelles, informatique théorique

  • Toulouse, 31400

  • CDD

  • 01/10/2025- 30/09/2028

Description

L’ENAC, École Nationale de l’Aviation Civile, est la plus importante des Grandes Écoles ou universités aéronautiques en Europe. Elle forme à un spectre large de métiers : des ingénieurs ou des professionnels de haut niveau capables de concevoir et faire évoluer les systèmes aéronautiques et plus largement ceux du transport aérien ainsi que des pilotes de ligne, des contrôleurs aériens ou encore des techniciens aéronautiques.

Ses laboratoires de recherche sont à la pointe de l’innovation et travaillent activement en coopération avec des universités internationales de haut niveau pour un transport aérien toujours plus sûr, efficace et durable.

L’ENAC est un établissement public à caractère scientifique, culturel et professionnel – grand établissement (EPSCP-GE), sous tutelle de la DGAC (Direction Générale de l’Aviation Civile), Direction du Ministère de la Transition Écologique et Solidaire. L’ENAC comprend une direction générale localisée à Toulouse et 8 sites en France.

 

Pour soutenir sa dynamique en faveur de la promotion de la diversité, l’ENAC facilite l’accueil et l’intégration des travailleurs en situation de handicap.

Mission

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és à 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.

 

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 liens 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.

 

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

 

En plus de ces tâches liées à la recherche, il sera également possible d’effectuer des enseignements à l’ENAC (avec complément de salaire).

Profil

·        Bac +5 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é)