Surveillance et vérification d'applications impliquant des jumeaux numériques // Monitoring and Verification of Applications involving Digital Twins

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. https://edtlab.fr/en/).

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. https://edtlab.fr/en/).

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/2026

Autres financements

Université Grenoble Alpes

217 MSTII - Mathématiques, Sciences et technologies de l'information, Informatique

Profil recherché : - Diplôme : Master 2 (M2) Recherche ou MSc en informatique ou dans un domaine étroitement lié. - Compétences clés : Solides bases en méthodes formelles et en vérification. - Informatique : Maîtrise de la programmation. - Langues : Bonne maîtrise de l'anglais comme langue de travail. - Qualités professionnelles : Excellentes capacités de communication, autonomie, rigueur (souci du détail) et esprit d'équipe. Compétences appréciées (atouts) : - Familiarité avec les méthodes probabilistes (par exemple, le model checking probabiliste, ou l'utilisation d'outils tels que PRISM ou Storm). - Connaissances en systèmes distribués et/ou en jumeaux numériques. - Expérience ou intérêt pour la robotique, l'automatique ou les systèmes cyber-physiques.
**Required:** - MSc / Master 2 Recherche in Computer Science or a closely related field - Solid background in formal methods and verification - Programming proficiency - Good command of English as the working language - Strong communication skills, autonomy, attention to detail, and a collaborative mindset **Appreciated:** - Familiarity with probabilistic methods (e.g., probabilistic model checking, tools such as PRISM or Storm) - Knowledge of distributed systems and/or digital twins - Exposure to robotics, control, or cyber-physical systems