Stage Utilisation Méthodes Model Checking pour les Procédures de Conduite des Centrales Nucléaires H/F - EDF

Contexte
EDF est un leader mondial de production d'électricité d'origine nucléaire. La sûreté de son parc des centrales nucléaires est une priorité majeure pour l'entreprise. Différents moyens : matériels, humains et organisationnels sont nécessaires pour garantir un haut niveau de sûreté .
Les procédures de conduite des centrales sont nécessaires pour guider l'équipe de conduite d'une centrale nucléaire en cas d'un incident.
La vérification des procédures de conduite (règles et consignes) des centrales nucléaires est donc un enjeu important pour EDF.
Avec la complexification de la réglementation, il devient de plus en plus difficile pour les rédacteurs de vérifier les procédures et d'instruire les impacts d'une modification sur l'ensemble du jeu de consignes et a fortiori sur la sûreté globale.
Le formalisme des statecharts [1] a été introduit par D. Harel a la fin des années 80 pour faciliter la modélisation et spécification des systèmes complexes [2].
La sémantique formelle d'exécution des statecharts permet de simuler le comportement du système et de vérifier si ce comportement est conforme aux spécifications [3, 4]. Grâce à leur caractère visuel, les statecharts facilitent l'analyse des comportements du système, la compréhension et la discussion des résultats par des spécialistes des différents domaines concernés.
A ce jour nous disposons d'un nombre limité de procédures de conduite accidentelle exprimés sous forme de statecharts avec des tests unitaires associés.

Objectif du stage
L'objectif global de ce projet de recherche est d'utiliser les techniques de model checking [6] sur les modèles des procédures exprimés en statecharts pour vérifier ces propriétés au-delà de ce que nous permettent de faire les tests. Pour cela, il est nécessaire d'adapter/interfacer une des solutions existantes [7] pour les modèles de procédures de conduite ainsi que de montrer la possibilité de vérifier un certain nombre de propriétés de la procédure. L'objectif du stage est de faire une étude bibliographique du sujet en se basant sur la documentation interne et la littérature externe ainsi que de faire une expérimentation avec un outil model checking existant[1] sur un échantillon restreint de la procédure de conduite. Ce travail pourra être poursuivi dans le cadre d'une thèse CIFRE[2] à partir du troisième trimestre de 2026.

Compétences développées au cours du stage
Ce stage permettra de développer des compétences transverses de spécifications, modélisation et vérification de systèmes complexes (ex. ingénierie des logiciels, aérospatial, nucléaire) ainsi que des connaissances dans le domaine du nucléaire, notamment celui du fonctionnement et de la conduite de centrales. Le.a candidat.e sera amené a travailler et échanger avec les différents métiers associés au sujet (ingénieurs sûreté, conduite, modélisation et facteurs organisationnels et humains).

En cursus Ecole d'ingénieur ou Universitaire Master 2, vous êtes à la recherche d'un stage de 5 à 6 mois en 2026. Dans votre parcours vous avez été exposé aux techniques de model-checking, vous avez pu utiliser un model checker existant (e.g. SPIN, UPPAAL). Votre implication, votre autonomie, votre curiosité sont attendues pour ce stage ; un regard critique sur les résultats est souhaité.
Les aspects informatiques relevant du stage seront la connaissance de langage de programmation (python, C, C++, ...). La connaissance de Java serait un plus.

Références
[1] Welcome to the world of Statecharts, https://statecharts.dev/
[2] David Harel, Statecharts: a visual formalism for complex systems, Science of Computer Programming, Volume 8, Issue 3, 1987, Pages 231-274
[3] Claudia Picoco, Valentin Rychkov, Model based software engineering techniques for dynamic reliability assessment, ESREL 2022 Dublin, DOI:10.3850/978-981-18-5183-4
[4] Claudia Picoco, Valentin Rychkov, Tunc Aldemir A framework for verifying Dynamic Probabilistic Risk Assessment models, Reliability Engineering & System Safety Volume 203, November 2020, 107099
[5] itemisCREATE tool itemis CREATE State Machine Tool - Lowcode Development
[6] Gérard Berry, La vérification de modèles (model-checking), Collège de France (college-de-france.fr)
[7] E. André et al., Formalizing UML State Machines for Automated Verification - A Survey, https://doi.org/10.1145/3579821