Thèse Interfaces Utilisateur Frugales et Vérifiables pour le Vol Autonome H/F - Doctorat.Gouv.Fr

Établissement : Ecole Nationale de l'Aviation Civile École doctorale : EDMITT - Ecole Doctorale Mathématiques, Informatique et Télécommunications de Toulouse Laboratoire de recherche : ENAC-LAB - Laboratoire de Recherche ENAC Direction de la thèse : Cyril ALLIGNOL ORCID 0000000175285512 Début de la thèse : 2027-09-01 Date limite de candidature : 2026-11-16T23:59:59 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'étudiante 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'étudiante é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. User interfaces for autonomous systems form part of the system's safety architecture. They communicate operating modes and warnings, support decision-making, and mediate transfers of control between human operators and autonomous functions. Their behaviour is driven by events, data dependencies, and changes to internal state. Interactions between these mechanisms can be difficult to predict and may generate large state spaces during formal analysis.

Smala is an interaction-oriented programming language in which interactive applications are constructed from processes connected by activations and data dependencies [1]. Its relatively small set of core mechanisms makes it a promising basis for studying how the design of an interface language affects both its semantics and the cost of formal analysis.

Previous collaboration between the University of Glasgow and the ENAC team has investigated bigraphs as a formal basis for Smala. In his doctoral work, Nalpon developed a bigraphical intermediate language and a translation of Smala programs into this representation [2]. Bigraphs represent both the organisation of a system and its evolution through rewriting. This makes them suitable for describing interfaces whose components, connections, and states evolve in response to events.

At the University of Glasgow, Sevegnani leads the development of BigraphER with his research group. The tool supports bigraph matching, rewriting, simulation, and visualisation [3]. Integrating the Smala encoding with BigraphER makes the generated semantics executable and allows its transition system to be explored. The proposed work will extend this integration, linking Smala programs directly to executable bigraphical models and their analysis in BigraphER.

The existing translation also allows language design to be studied quantitatively. For each Smala construct, it is possible to observe the reactions, intermediate states, and branching introduced by its bigraphical representation. These measurements can distinguish externally meaningful interface behaviour from internal activity required by the language semantics or its encoding. This can identify language constructs that generate unnecessary complexity during analysis.

Frugality applies to both the language and its verification. A concise language construct may produce many states that are irrelevant to the safety property being checked, increasing analysis time and memory use. Such costs can prevent formal methods from being used repeatedly during development or applied to larger and more realistic interfaces. The project will consider the Smala language, its bigraphical semantics, and its integration with BigraphER together.

Reducing these costs could make formal assurance practical for a wider range of future air-mobility systems. The connection with sustainable transitions comes from enabling trustworthy autonomous technologies to be developed and assessed at realistic scales, using assurance methods whose computational and engineering demands do not prevent their wider adoption.

Any reduction must retain the safety claims made about the original program. A smaller state space is of limited value if it omits relevant behaviours or produces results that cannot be related to the Smala source. BiCoq provides a machine-checked formalisation of core bigraph operations [4], with ongoing work extending this foundation to bigraph rewriting. This foundation can support proofs that changes to the language, its encoding, or its analysis preserve safety-relevant behaviour. Existing work on probabilistic, action, and real-time bigraphs provides possible foundations for later extensions concerning uncertainty and response deadlines [5,6]. Research question :

* How can the semantic and verification costs of Smala constructs be measured through their bigraphical representation and its execution in BigraphER?

The project will investigate measures including internal reactions, intermediate states, branching, reachable states, memory use, and analysis time. It will also consider how to distinguish observable interface behaviour from administrative steps introduced by the semantics.

* How can Smala and its integration with BigraphER be revised to reduce unnecessary semantic activity and state-space exploration while preserving safety-relevant behaviour?

Possible approaches include redesigning expensive language mechanisms, collapsing sequences of internal reactions, exploiting compositional structure, and generating models containing only behaviour relevant to a given property. Formal results will relate the revised language and reduced models to the existing semantics.

* Can frugal programming and verification support wider adoption of trustworthy assurance methods in future air mobility?

The revised approach will be evaluated on autonomous-flight interfaces involving warnings, operating modes, and human-autonomy handovers. The evaluation will examine whether the time, memory, and engineering effort required to establish safety properties can be reduced without weakening the properties checked. Work plan:

* Year 1: Toulouse

The first year will establish the technical baseline. The student will study Smala, bigraphical reactive systems, the existing Smala encoding, and its execution with BigraphER. They will reproduce existing examples and develop instrumentation for recording semantic steps, intermediate states, branching, and state-space growth.

Working with ENAC researchers, the student will define a set of representative autonomous-flight interface scenarios. These are expected to cover warnings, changes of operating mode, competing events, and transfers of control. Each scenario will describe required and prohibited behaviours together with suitable safety properties.

The student will use these scenarios to characterise the current approach. The resulting measurements will identify the Smala mechanisms and aspects of the encoding that contribute most to semantic and verification costs.

* Year 2: Glasgow

The student will undertake an extended research placement at the University of Glasgow. This phase will focus on revising the bigraphical encoding and integrating the resulting analysis methods with BigraphER.

Using the first-year measurements, the student will investigate simpler treatments of semantically expensive Smala mechanisms. They will also develop methods for avoiding unnecessary exploration of internal or property-irrelevant behaviour. Candidate changes will be evaluated against the same interface scenarios to ensure that reductions in reactions or reachable states are not obtained by removing required behaviour.

The student will formulate and begin proving results that relate revised programs and reduced bigraphical models to the original semantics. These may use operational correspondence, trace preservation, or an equivalence that abstracts from internal steps. BiCoq may support machine-checked parts of the argument where a formal treatment of bigraph operations or rewriting is useful.

* Year 3: Toulouse

The final year will consolidate the formal results and evaluate the proposed methods on more substantial autonomous-flight interfaces. The evaluation will compare the original and revised approaches using semantic steps, reachable states, analysis time, memory use, and the safety properties retained.

The student will document the supported language fragment and the assumptions under which the reductions are valid. Depending on progress, the project may also consider timed behaviour for warnings and human responses, building on existing work on real-time bigraphs.

Les candidates doivent avoir des compétences solides en informatique fondamentale ou mathématiques, être à l'aise avec le raisonnement mathématique, et avoir de l'expérience dans au moins l'un des domaines suivants :
- logique mathématique ou mathématiques discrètes ;
- modélisation et vérification formelles ;
- sémantique des langages de programmation ;
- transformations et ré-écritures de graphes ;
- model checking ou assistants de preuves.

Des compétences solides en programmation sont requises. Une expérience de la programmation fonctionnelle, préférentiellement en OCaml, serait utile mais n'est pas essentielle. Il n'est pas attendu des candidates une expérience avec les bigraphes, Smala ou les systèmes aéronautiques.