STAGE Utilisation méthodes Model Checking pour les procédures de conduite des centrales nucléaires F/H
> EDFStage 6 Mois Ingénierie Palaiseau A définir
Détails de l'offre
Présentation de l'entreprise
Le groupe EDF est l'un des premiers électriciens mondiaux, à la pointe de l'innovation technologique. Le respect de la personne et celui de l'environnement, l'intégrité, la solidarité sont au cœur de nos actions. Face à l’urgence climatique, notre rôle est d’inventer un modèle énergétique qui respecte notre planète.
Nous voulons construire un monde où il sera possible de produire une électricité neutre en CO2, grâce au nucléaire et aux énergies renouvelables, conciliant préservation de la planète, bien-être et développement, grâce à l’électricité et à des solutions et services innovants.
Pourquoi nous rejoindre ? 😀
Rejoindre EDF, c’est travailler dans un Groupe qui lutte au quotidien contre le réchauffement climatique. C’est travailler dans un Groupe avec des valeurs fortes qui innove avec de solides actifs industriels et vous confie des missions qui ont du sens. Rejoindre EDF, c’est partager une aventure ensemble.
Missions
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).
Profil recherché
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