Thèse Surveillance et Vérification d'Applications Impliquant des Jumeaux Numériques H/F - Doctorat.Gouv.Fr

Établissement : Université Grenoble Alpes École doctorale : MSTII - Mathématiques, Sciences et technologies de l'information, Informatique Laboratoire de recherche : Laboratoire d'Informatique de Grenoble Direction de la thèse : Gwen SALAUN ORCID 0000000336548791 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-06-30T23:59:59 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). Digital twins, formal methods. Développer des approches formelles pour les jumeaux numériques.

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.

• Programmation