Thèse Jumeaux Numériques de Confiance pour les Transitions Énergétique et Aéronautique - Commande Robuste et Garanties Formelles de la Conception à l'Exploitation. H/F Doctorat.Gouv.Fr

Établissement : Ecole Nationale de l'Aviation Civile École doctorale : SYSTEMES Laboratoire de recherche : ENAC-LAB - Laboratoire de Recherche ENAC Direction de la thèse : Pierre-Loïc GAROCHE ORCID 0000000205136076 Début de la thèse : 2027-09-01 Date limite de candidature : 2026-11-23T23:59:59 La transition écologique impose aux systèmes physiques d'être plus sobres en
énergie, tandis que la transition numérique les rend de plus en plus
automatisés. Une éolienne doit extraire le maximum d'énergie d'un vent très
variable tout en maîtrisant les charges mécaniques, la fatigue et la sécurité ;
en aéronautique, réduire la consommation et les émissions suppose une commande
plus fine et davantage d'autonomie, sous de fortes contraintes de sécurité. Dans
les deux cas, les ingénieurs souhaitent faire fonctionner les systèmes au plus
près de leur optimum sans perdre les garanties qui assurent leur sûreté.

Les jumeaux numériques - des modèles maintenus en correspondance avec un système
physique tout au long de sa vie - sont un outil naturel pour cela, mais servent
aujourd'hui surtout à la simulation et à l'optimisation. Il manque en général un
lien rigoureux entre ce que prédit le modèle et le comportement réel du système,
une fois pris en compte erreurs de modélisation, perturbations, variations de
paramètres, vieillissement et effets d'implémentation logicielle.

Cette thèse développe des jumeaux numériques de confiance qui portent des
garanties mathématiques, de la conception à l'exploitation. Elle combine trois
briques matures mais rarement intégrées : la commande robuste et les contraintes
quadratiques intégrales (IQC) pour raisonner sur l'effet des incertitudes ; la
vérification formelle (ensembles invariants, analyse d'atteignabilité,
certificats de Lyapunov et Sum-of-Squares, preuves au niveau du code) pour
transformer les arguments de la théorie de la commande en certificats
vérifiables ; et le jumeau numérique comme infrastructure portant ces
certificats le long du cycle de vie conception vérification implémentation
exploitation.

Quatre objectifs structurent le travail : (O1) construire des jumeaux numériques
conscients de l'incertitude ; (O2) produire des certificats robustes de
stabilité, de performance et de respect des contraintes exploitables par des
outils de vérification ; (O3) calculer des enveloppes opérationnelles certifiées
(ensembles invariants et atteignables des boucles fermées incertaines) de façon
aussi automatique que possible ; (O4) utiliser les mesures d'exploitation pour
vérifier la validité des hypothèses d'un certificat et mettre à jour l'enveloppe
certifiée - une « enveloppe de sécurité vivante ».

La méthodologie, indépendante du domaine, est démontrée sur deux applications
complémentaires : les systèmes éoliens (cas d'étude principal, transition
écologique) et les systèmes aéronautiques (test de transférabilité, autonomie
sûre et sobre en énergie), ces derniers sur un banc hélicoptère Quanser 3 DDL
disponible à l'ENAC et à l'AUB.

Le projet s'appuie sur une collaboration établie entre l'ENAC (P.-L. Garoche :
méthodes formelles, atteignabilité, certification) et l'AUB (D. Abou Jaoude :
commande robuste, IQC, systèmes éoliens), qui ont déjà co-signé deux articles sur
les ensembles invariants sous IQC, sans financement commun ; BEST serait leur
premier projet financé conjointement. La thèse, de 36 mois, est préparée à
Toulouse avec un séjour d'environ deux mois par an à l'AUB.

Résultats attendus : une méthodologie reliant commande robuste et vérification
formelle au sein des jumeaux numériques ; des enveloppes de fonctionnement sûres
certifiées obtenues à partir de descriptions d'incertitude ; une méthode de
validation et de mise à jour des certificats en exploitation ; un prototype
logiciel ouvert reliant conception, analyse robuste, certification et
supervision. Enjeu sociétal : des systèmes plus efficaces (fonctionnement au plus
près de l'optimum) et plus sûrs (marges quantifiées). Robust control and IQCs. Robust-control theory designs controllers that keep stability and per-
formance despite uncertainty; IQCs [9, 12] give a flexible way to characterise uncertain, nonlinear and interconnected components and to analyse the resulting closed loop. These tools provide robustness margins but do not, by themselves, certify that all physical constraints stay satisfied [13].

Formal verification of dynamical and cyber-physical systems. Reachability analysis, invariant-
set computation, Lyapunov reasoning and optimisation-based certificates such as Sum-of-Squares and semidefinite programming [10] produce mathematical proofs of safety and stability beyond what simulation or testing can show.

Digital twins. Existing digital-twin approaches range from high-fidelity simulators to operational
models continuously fed by measurements [3, 7]. The rigorous connection between a digital twin and formal guarantees - especially the question of whether a design-time certificate is still valid once the system is deployed and ageing - remains largely open.

What the two teams already own. This project builds on a joint line of work by the two supervisors:

- IQC-based invariant sets for uncertain systems. Together, the teams introduced the computation of state invariants for uncertain systems using point-wise IQCs and the S-procedure [2], and extended it to invariant-set computation for discrete-time uncertain systems [6].
- Certified reachability and SOS/SDP. On the Toulouse side, semidefinite approximations of reach-
able sets for polynomial systems [8] and parabolic-set reachability under IQCs [11].
- From certificate to code. Also on the Toulouse side, code-level formal verification of ellipsoidal
invariant sets for LPV systems [4] and formal proofs of invariant systemic properties of control pro-
grams using ghost code and IQCs [5], building on a reference monograph on the formal verification of control-system software [1].
- Robust control and wind energy. On the AUB side, robust control, IQC/dissipativity-based analysis of uncertain and nonlinear systems, and the modelling and control of wind-energy systems.

The PhD extends this shared foundation in a new direction: from static certificates computed once at design time to a lifecycle digital twin whose guarantees are carried through implementation and kept valid - or explicitly updated - during operation. The ecological transition requires physical systems to become more energy-efficient, while the digital transition makes them increasingly automated. Wind turbines must extract as much energy as possible from highly variable wind while keeping mechanical loads, fatigue and safe operation under control; in aeronautics, reducing fuel consumption and emissions similarly relies on more aggressive control and more autonomy under stringent safety constraints. In both cases, engineers would like to operate systems closer to their optimum without losing the guarantees that keep them safe.

Digital twins - digital models kept in correspondence with a physical system throughout its life -
are a natural tool for this, but are used today mostly for simulation and optimisation. What is generally missing is a rigorous link between what the digital model predicts and how the real system behaves, once modelling errors, disturbances, parameter variations, ageing and software-implementation effects are taken into account.

Central question. How can a digital twin be equipped with mathematical guarantees,
so that it supports not only simulation but also the trustworthy design, verification and
operation of an uncertain controlled system?

The thesis combines three mature but rarely integrated ingredients: robust control and Integral
Quadratic Constraints (IQCs) to reason about the effect of uncertainty on dynamical systems;
formal verification(invariant sets, reachability analysis, Lyapunov / Sum-of-Squares certificates, code-level proofs) to turn control-theoretic arguments into checkable mathematical certificates; and digital twins as the infrastructure that carries these certificates along the lifecycle design verification implementation operation.

The scientific objectives are:

O1 - Uncertainty-aware digital twins. Build digital representations of controlled systems that ex-
plicitly model the uncertainties relevant to stability, performance and safety, at the level of fidelity
actually required by a given guarantee.

O2 - Robust certificates. Combine robust control, IQC and dissipativity/Lyapunov techniques to
produce quantitative guarantees on stability, robustness, performance and constraint satisfaction,
in a form that formal-verification tools can exploit.

O3 - Certified operating envelopes. Compute certified invariant and reachable sets for uncertain
closed loops - the region in which the system is guaranteed to remain under specified disturbances - as automatically as possible from a model, an uncertainty description, a controller and requirements.

O4 - From static certificate to operational guarantee. Use measurements collected during operation to test whether the assumptions behind a certificate still hold, and to update the uncertainty bounds and the certified envelope: a living safety envelope.

The methodology is domain-independent. It is demonstrated on two complementary applications:
wind-energy systems (primary case study, ecological transition) and aerospace systems (transfer-
ability test, safety-critical and energy-efficient autonomy), the latter on a Quanser 3-DOF helicopter benchmark available both at ENAC and AUB. Layer 1 - Model-based design. Construct digital twins of the wind-turbine and helicopter bench-
marks containing physical dynamics, controller, actuators, sensors, disturbances, parameter uncertainties and operational constraints. Determine which model fidelity a given guarantee actually requires, so that the digital twin also supports sizing (actuator authority, sampling rate, component characteristics) rather than only after-the-fact validation.
Layer 2 - Robust control and uncertainty characterisation. Describe uncertain components
(uncertain parameters, unmodelled dynamics, nonlinearities, disturbances, interconnections) with IQCs and dissipativity, and derive quantitative robustness and performance certificates, combined with Lyapunov arguments.
Layer 3 - From robustness to formal safety guarantees. Compute certified invariant and
reachable sets X_{safe} for the uncertain closed loop, using SOS/SDP and the S-procedure/IQC techniques the teams have developed, with emphasis on automation and, where relevant, on verifying the resulting certificates at code level.
Layer 4 - Operational digital twin. Use operational measurements to check whether the uncer-
tainty assumptions behind a certificate still hold, to re-estimate uncertainty bounds (robust identification, interval and set-membership methods) and to update the certified envelope. No machine learning is required: estimation, reachability and formal reasoning are sufficient.

Indicative milestones (36 months).

Year 1 (M1-M12) - State of the art and benchmarks. Survey; uncertainty-aware digital twins
of the wind-turbine and Quanser 3-DOF helicopter benchmarks with requirements and uncertainty
models; first robust-control / IQC stability and robustness certificates; baseline invariant-set and
reachability tooling.
Deliverable: benchmark digital twins + first robust certificates. Expected paper: IQC / robust-
control analysis of the benchmarks.

Year 2 (M13-M24) - Formal certification and wind-energy demonstrator. Automatedcom-
putation of certified invariant/reachable sets for uncertain closed loops; code-level verification of
the certificates; start of lifecycle integration (design-time vs implementation-level models, model-
discrepancy study); application to wind-turbine control and to the energy/load trade-off.
Deliverable: prototype certification framework + wind-energy case study. Expected paper: certified
operating envelopes for uncertain controlled systems.

Year 3 (M25-M36) - Operational digital twin, aerospace transfer, consolidation. Livingsafety
envelope using operational data; transfer of the methodology to the aerospace benchmark (energy-efficient control, flight-envelope protection); open-source prototype linking model-based design, robust analysis and formal verification; dissemination and thesis writing.
Deliverable: lifecycle certified digital twin + two demonstrators + thesis.

Organisation. The student is recruited in and based at ENAC (Toulouse), with a secondment of about two months per year at AUB for the robust-control / IQC and wind-turbine components, and regular joint supervision meetings. Tools: Python / MATLAB / Julia, SDP and SOS solvers, reachability and formal-verification tools, and open turbine models (e.g. the NREL/OpenFAST ecosystem).