Interfaces utilisateur frugales et vérifiables pour le vol autonome

La sécurité des vols autonomes repose notamment sur des interfaces humain-machine qui permettent aux opérateurs de comprendre l'état du système, réagir à des alertes et prendre ou rendre le contrôle. Cependant, les interactions entre les événements externes et l'état interne du système peuvent générer des modèles de comportement immenses, ce qui peut rendre coûteuse leur analyse vis-à-vis des objectifs de sécurité. Cette thèse s'intéresse à une approche frugale de la programmation et de la vérification d'interfaces critiques du point de vue de la sécurité. Cette approche se base sur des travaux existants de traduction de programmes écrits dans le langage Smala vers les bigraphes, ainsi que de leur exécution et leur analyse à l'aide de BigraphER. Cette traduction explicite les étapes internes ainsi que les états intermédiaires inhérents à chaque construction du langage, permettant ainsi de mesurer le coût de leur sémantique et de leur vérification. L'étudiant⋅e utilisera ces mesures afin d'identifier les constructions les plus coûteuses, développer des alternatives plus simples, et réduire l'espace d'état exploré lors de la vérification de propriétés de sécurité. Il/elle devra assurer que ces changements préservent le comportement du programme original, en utilisant des outils de preuve assistée. Au sein de l'ENAC, l'étudiant⋅e évaluera son approche sur des scénarios de vol autonome, impliquant des alertes, des modes d'opération variés, ainsi que des transferts entre les modes autonome et piloté. En réduisant les coûts de développement et d'exécution de la vérification, ce projet aide à l'adoption de méthodes fiables pour les systèmes de mobilité aérienne futurs. École doctorale : EDMITT - Ecole Doctorale Mathématiques, Informatique et Télécommunications de Toulouse Direction : Cyril ALLIGNOL Financement : MSCA COFUND BEST