Topic description
Un jumeau numérique est la représentation virtuelle d'une entité du monde réel. Il est souvent présenté comme un outil prédictif, permettant de simuler de multiples scénarios possibles pour cette entité. Dans un tel contexte, il est essentiel que le jumeau numérique adopte un comportement fidèle à celui du système qu'il cherche à imiter. Tout écart significatif et durable entre le jumeau et son homologue concret peut conduire à des prédictions erronées, à de faux diagnostics et, de manière générale, à une mauvaise perception du fonctionnement du système réel. Les techniques actuelles ne répondent pas au besoin de méthodes d'analyse prenant en charge des modèles hétérogènes et fournissant un retour pertinent sur l'exactitude et la qualité des modèles intégrés au sein du jumeau numérique.
Le changement de paradigme majeur que nous poursuivons dans cette thèse consiste à ne pas traiter le jumeau numérique comme un artefact statique, validé une fois pour toutes lors de la phase de conception, mais comme un modèle vivant qui coévolue avec les observations au fil de l'eau (au moment de l'exécution), tout en offrant des garanties formelles à la fois sur la détection des écarts et sur la prédiction des comportements futurs.
L'objectif de cette thèse de doctorat est de travailler sur les deux sujets connexes suivants :
- Détection des écarts par l'utilisation de techniques de surveillance et de vérification à l'exécution (runtime verification). Nous utiliserons à la fois les modèles disponibles dans le jumeau numérique et les informations/données concrètes provenant des systèmes réels afin d'identifier des changements ou des évolutions dans le comportement des applications réelles. Ces informations pourront être exploitées pour la maintenance prédictive ou pour la mise à jour des modèles qui s'écartent des modèles originaux.
- Gestion de l'incertitude par le biais du Model Checking Probabiliste (PMC). Le comportement de l'environnement dans les systèmes physiques est crucial pour mieux comprendre et contrôler les applications concernées. Le PMC s'appuie sur des modèles probabilistes calculés à partir des modèles disponibles dans le jumeau numérique et des données récupérées depuis les systèmes physiques. Ces modèles permettent la vérification de propriétés probabilistes, dont les résultats peuvent être visualisés sur un tableau de bord pour observer l'exécution des systèmes et servir à l'adaptation de leur comportement en temps réel.
Ces deux axes sont interconnectés par une boucle commune de mise à jour des modèles : les verdicts produits par la surveillance en temps réel alimentent la réestimation probabiliste des paramètres de l'environnement et du système, tandis que les prédictions du PMC guident la synthèse et l'adaptation des moniteurs déployés à l'exécution.
Toutes les contributions apportées au cours de cette thèse seront validées par des prototypes d'outils et appliquées à des cas d'étude réalistes. En particulier, nous prévoyons de travailler sur un cas d'étude impliquant des drones — combinant simulation et plateformes physiques — dans le but d'améliorer leurs systèmes de navigation et d'éviter les comportements anormaux tels que les collisions, les trajectoires sous-optimales et les pertes de contrôle (flyaways).
Cette thèse de doctorat s'inscrit dans le cadre du projet SYNCRONIC du programme national français « Ingénierie des Jumeaux Numériques » (EDT, cf.
La thèse sera coencadrée par Gwen Salaün et Yliès Falcone, combinant ainsi des expertises en méthodes formelles pour les systèmes distribués et concurrents, en vérification à l'exécution et en application de propriétés (enforcement).
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
A digital twin is a virtual representation of a real-world entity. It is often
presented as a predictive instrument, by enabling one to simulate multiple
possible outcomes of a real-world entity. In such a context, it is essential
that the digital twin exhibits behavior that is faithful to that of the system
it seeks to mimic. Any significant and sustained discrepancy between the twin
and its concrete counterpart can lead to incorrect predictions, false diagnoses,
and generally to an incorrect perception of the real system operation.
Current techniques fall short of meeting the need for analysis methods
that support heterogeneous models and provide meaningful feedback on the
correctness and quality of the models embedded within the digital twin.
A key shift we pursue in this thesis is to treat the digital twin not as
a static artifact validated once at design time, but as a live model that
co-evolves with runtime observations, with formal guarantees on both the
detection of deviations and the prediction of future behavior.
These techniques face several challenges. First, the expressiveness and
heterogeneity of models, as well as the coupling between composite
components, complicate both modeling and analysis. Second, environmental
uncertainty makes the behavior of such models difficult to predict.
The goal of this PhD thesis is to work on the two following related topics:
- Detection of deviations by using monitoring and runtime verification
techniques. We will use both the available models in the digital twin with
concrete information/data coming from real systems to identify some changes or
evolutions in the behavior of real applications. This information can be used
for predictive maintenance or for updating models that deviate from the original
ones.
- Uncertainty management by using Probabilistic Model Checking (PMC).
The behavior of the environment in physical systems is crucial to better
understand and control the applications at hand. PMC relies on probabilistic
models computed from models available in the digital twin and data retrieved
from the physical systems. These models allow the verification of probabilistic
properties, whose results can be visualized on a dashboard for observation of
the systems' executions and use for runtime adaptative behavior.
The two strands are connected through a shared model-update loop: runtime
verdicts produced by monitoring inform the probabilistic re-estimation of
environment and system parameters, while PMC predictions guide the synthesis
and adaptation of monitors deployed at runtime.
All contributions made during this PhD will be validated via prototype tools
and applied to realistic case studies. In particular, we plan to work on a
case study involving drones, combining simulation and physical platforms,
with the goal of improving their navigation systems and avoiding abnormal
behaviors such as collisions, sub-optimal trajectories, and flyaways.
This PhD thesis is part of the SYNCRONIC project of the nationwide French
program 'Engineering Digital Twins' (EDT, cf.
The thesis will be co-supervised by Gwen Salaün and Yliès Falcone, combining
expertise in formal methods for distributed and concurrent systems with
runtime verification and enforcement.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
Début de la thèse : 01/10/
Funding category
Funding further details
Autres financements
En cliquant sur "JE DÉPOSE MON CV", vous acceptez nos CGU et déclarez avoir pris connaissance de la politique de protection des données du site jobijoba.com.