Thèse Façonner l'Ingénierie des Futurs Systèmes Critiques à l'Aide d'Approches d'IA Fondées sur des Bases Mathématiques H/F - Télécom Paris

Établissement : Télécom Paris
École doctorale : Ecole Doctorale de l'Institut Polytechnique de Paris
Laboratoire de recherche : Laboratoire de Traitement et Communication de l'Information
Direction de la thèse : Ludovic APVRILLE ORCID 0000000211674639
Début de la thèse : 2026-10-01
Date limite de candidature : 2026-06-30T23:59:59

Les systèmes critiques (aéronautique, nucléaire, médical, défense) sont soumis à des contraintes très strictes, car une défaillance peut avoir des conséquences humaines, environnementales et économiques majeures, comme l'ont illustré les accidents du Boeing 737 MAX liés au MCAS. Leur conception est encadrée par des normes et réglementations rigoureuses. En parallèle, l'IA, et en particulier les grands modèles de langage (LLM), s'impose dans les processus d'ingénierie. Ils promettent des gains importants, mais leurs biais et hallucinations sont incompatibles avec les exigences de sûreté de ces domaines. Il faut donc des solutions permettant une intégration sûre et conforme aux standards.

Le travail se situe à l'interface entre l'Ingénierie Dirigée par les Modèles (MDE) et les Méthodes Formelles, pour la conception de systèmes critiques. La MDE utilise des modèles pour capturer exigences, architectures et comportements, les analyser (simulation, vérification formelle) et générer du code. Les méthodes formelles (par exemple le model checking) apportent une base mathématique pour spécifier et vérifier la correction. Leur combinaison fait de la MDE une approche rigoureuse adaptée aux systèmes hautement critiques.

Télécom Paris développe depuis plus de 20 ans TTool, un environnement MDE fondé sur les méthodes formelles. L'équipe l'a récemment étendu avec TTool-AI, un assistant intégrant des LLM pour, entre autres, générer des modèles à partir de spécifications textuelles, produire des arbres d'attaque, vérifier la cohérence de modèles hétérogènes et traduire des exigences en propriétés temporelles. TTool-AI s'appuie sur des connaissances métier, la vérification automatique de la syntaxe et de la sémantique, et une boucle de rétroaction qui corrige les sorties jusqu'à atteindre un niveau de fiabilité donné.

Aujourd'hui, les approches existantes assurent surtout la correction syntaxique des modèles générés, laissant la plupart des aspects sémantiques aux ingénieurs. L'objectif de la thèse est de concevoir une approche MDE nouvelle, combinant IA et méthodes formelles, pour construire des modèles corrects par construction et renforcer la sûreté et la sécurité des systèmes critiques. Elle intégrera au moins deux mécanismes de vérification complémentaires (sûreté de fonctionnement et cybersécurité), reposera sur une base mathématique générale, sera implémentée dans TTool comme preuve de concept, et évaluée sur des cas d'étude représentatifs en interaction avec les partenaires industriels du LabSoC.

The proposed work anchors at the intersection of two scientific domains: Model-Driven Engineering (MDE) and Formal Methods, in the context of the design of critical systems. MDE is a system engineering approach for managing complexity that relies on models, i.e., abstractions of the systems under design, to rigorously reason about the architecture and behavior of the systems before they are put in exploitation. In MDE, engineers rely on models to capture and analyze system requirements, define functional architectures, and design software and hardware components. These models can then be validated through simulation or formal verification to assess whether the proposed designs satisfy the specified requirements. In addition, models can be used to automatically generate source code for software components. To increase the reliability of these processes, MDE often incorporates formal methods at both modeling and verification stages.
Formal methods rely on mathematical abstractions to formally specify, reason about, and verify system correctness. Among these techniques, model checking [4, 2] is particularly well known; it verifies system models (typically expressed as a set of timed automata) against properties expressed in temporal logic. Formal methods are com- monly integrated into MDE at three levels: (1) by defining modeling languages with precise mathematical semantics, (2) by translating requirements into temporal logic properties, and (3) by applying formal verification techniques such as model checking during model analysis. The convergence of these two fields makes MDE a rigorous engineering approach well suited to the development of highly critical systems.
For more than 20 years, Télécom Paris has developed and maintained a formal methods-based MDE toolkit called TTool [1]. TTool supports all stages of the MDE process and has been widely used in both industrial and academic settings. Over the past three years, our team has extended TTool with an AI-based systems engineering assistant named TTool-AI, and has published their results in reknown conferences and journal [7, 6]. TTool-AI integrates LLMs to assist engineers in several tasks, such as automatically translating textual specifications into architectural and behavioral models, generating attack trees for cybersecurity analysis, verifying the semantic consistency of heterogeneous models representing the same system, and translating requirements into temporal logic properties. TTool-AI relies on three core mechanisms: (1) generation of LLM augmented with domain-specific knowledge, (2) automated verification of LLM outputs against formal syntactic and semantic consistency rules, and (3) a feedback loop that reinjects detected inconsistencies into the prompts until the generated results meet a required level of reliability. The validated responses are then automatically parsed and converted into models within TTool.

LLMs are becoming, and will continue to be, increasingly central to systems engineering workflows. Our guiding principle is that their integration into critical systems engineering must be tightly coupled with formal methods, by constraining their outputs through mathematically grounded verification techniques. This PhD project aligns with this perspective.

Current LLM-based model-driven engineering assistance approaches primarily focus on ensuring the syntactic correctness of AI-generated models, while leaving most aspects of semantic correctness (i.e., conformance to system requirements) to engineers. This process is tedious. Enabling the construction of correct-by-construction models would significantly improve the quality of system architectures and enhance the reliability of LLM-based MDE assistants used by systems engineers.
Several works have undertaken first steps toward this direction [5, 3]. However, to the best of our knowledge, no existing approach integrates formal verification within the automatic and iterative LLM assistant model construction loop. The primary objective of this PhD project is therefore to design a novel AI- and formal methods- based MDE approach that support the development of safe and secure critical systems with a high degree of confidence. The proposed approach will include at least two complementary formal verification mechanisms to address both system safety and cybersecurity concerns.
The research will blend both theoretical and practical research work. It will proceed iteratively and could include for instance the following suggested steps:

- Define a rigorous mathematical foundation for the approach, extending for in- stance current formalizations [8, 6] in order to (1) establish a universal, tool- agnostic framework and (ii) enable formal reasoning about semantic model evolution and correctness preservation across the different steps of the approach.

- Integrate the framework into TTool to provide a robust proof of concept.

- Evaluate the framework on representative case studies from critical systems engineering, and interact with the LabSoC industrial partners.

- Goût pour la recherche à la fois théorique et appliquée
- Compétences techniques en informatique
- Compétence en systèmes embarqués (logiciel ou matériel)
- Compétence en cybersécurité (ou envie d'apprendre)