CRAN - Campus Sciences
BP 70239 - 54506 VANDOEUVRE Cedex
Tél : +33 (0)3 72 74 52 90 Fax : +33 (0)3 72 74 53 08
cran-secretariat@univ-lorraine.fr
 
 
Sujet de Thèse : Génération, vérification formelle et simulation de séquences de conduite pour un système complexe critique
Dates : 2013/10/01 - 2017/12/13
Etudiant : Thomas COCHARD
Directeur(s) CRAN : Jean-François PETIN , David GOUYON
Description : Contexte industriel

Le sujet de thèse proposé s’inscrit dans le cadre du projet CONNEXION « Contrôle-commande Numérique Nucléaire pour l'export et la rénovation » financé par la DGCIS (Devic & Morilhat 2013). Ce projet de R&D sur 4 ans regroupe les principaux acteurs (universitaires et industriels) de la filière française du contrôle-commande nucléaire (CEA, INRIA, CRAN, ENS Cachan, LIG, Télécom ParisTech, EDF, AREVA, ALSTOM, Atos, Rolls-Royce, Corys, Esterel, All4Tec, Predict) avec pour objectif de proposer une démarche de conception et de validation d’une architecture innovante de contrôle-commande sûr et performant, et permettant de développer une gamme de solutions compatibles export/rénovation. Le travail proposé dans cette thèse est une contribution aux activités d’un lot de travail intitulé « Vers l’intégration de nouveaux services métiers pour la performance des métiers de l’exploitation».

La description du fonctionnement des systèmes complexes tels que les centrales de production d’électricité (Lind et al. 2011) est consignée par des énoncés dans une note de fonctionnement général. Un premier pas vers la formalisation du fonctionnement a été réalisé par EDF/DER de manière graphique à l’aide d’outils de visualisation (Galara 2011). Ils mettent en œuvre des schémas dont l’intérêt offrant une représentation visuelle des domaines de fonctionnement et de l’état de fonctionnement des équipements. En revanche, ces représentations restent statiques dans le sens où les évolutions ne sont pas représentées de manière formelle.
En complément à cette visualisation, la formalisation du fonctionnement logique de la tranche pourrait apporter des moyens supplémentaires pour :
- valider le fonctionnement grâce au parcours des différents chemins dans le diagramme des situations d’exploitation nominale des systèmes, pour :
o détecter d’éventuelles situations de blocage en conduite ;
o vérifier qu’une situation d’exploitation reste atteignable ;
o identifier des consignes de conduite pouvant conduire à des situations interdites ;
o valider le dimensionnement des systèmes en particulier pour les situations d’exploitation nécessitant le fonctionnement simultané de plusieurs systèmes.
- faciliter la définition des états et des configurations des circuits lors du passage d’un domaine d’exploitation à un autre,
- faciliter la formation au fonctionnement, par exemple par simulation.

Objectifs scientifiques

Pour répondre aux objectifs industriels identifiés au paragraphe précédent, deux aspects complémentaires devront être abordés :
- la modélisation, pour proposer un formalisme permettant la représentation de tous les concepts et objets utilisés par les métiers de ma conduite,
- la validation, pour définir des mécanismes de simulation et de vérification formelle applicables sur les formalismes de représentation proposés.

En ce qui concerne la modélisation, les principales difficultés proviendront :
- de la nature hétérogène des objets et concepts à modéliser : en effet, s’il apparaît naturel de s’appuyer sur les modèles dynamiques des Systèmes à Événements Discrets (Cassandras & Lafortune 2008), pour manipuler les notions d’état et de transitions entre états, la description des domaines de fonctionnement caractérisés, entre autre, par des plages de grandeurs physiques nécessitera des formalismes manipulant des variables réelles ou a minima entière et leurs évolutions dans le temps. Les familles de modèles de SED hybrides et/ou temporisés sont susceptibles de répondre à ces besoins ;
- de la prise en compte des différents niveaux de hiérarchisation du fonctionnement d’une tranche qui nécessitera la définition de mécanismes :
o d’agrégation permettant d’élaborer une situation à un niveau donné en fonction des situations des niveaux inférieurs ;
o de maillage des différents modèles de représentation du fonctionnement logique. En effet, la structuration proposée n’est pas une décomposition hiérarchique par exemple au sens du modèle Statecharts (Harel 1988), mais repose plutôt sur un maillage des modèles pour lequel un modèle peut faire appel à un modèle de niveau inférieur depuis n’importe lequel de ses états et pas nécessairement dans les mêmes conditions ni avec les mêmes effets. Les mécanismes recherchés s’apparentent aux mécanismes d’instanciation et de synchronisation offerts par le formalisme « automate à états finis communicants » (Alur & Dill 1994).

Le formalisme proposé devra être apte à répondre à l’ensemble de ces exigences.
En ce qui concerne la validation, il s’agira essentiellement d’adapter au formalisme de modélisation proposé des capacités :
- de vérification formelle basée sur l’exploration de l’espace d’états, par exemple des techniques de recherche d’atteignabilité ou plus généralement de model-checking (Marangé et al. 2009) ;
- de simulation, basée sur une exécution « temps réel » du modèle logique.

Travail de thèse

L’objectif de la thèse est de contribuer à la définition de formalismes de représentation répondant à des objectifs de simulation et de vérification formelle de séquences de conduite. Le doctorant proposera en ce sens un modèle formel du fonctionnement logique d’une tranche en s’appuyant sur ces formalismes, avec l’aide d’EDF/DER pour les aspects relevant d’une compétence « métier ».

Pour atteindre cet objectif, plusieurs phases de travail sont envisagées :
- étude bibliographique des modèles à états couvrant tout ou partie des besoins exprimés en modélisation et vérification,
- méta-modélisation des concepts manipulés pour décrire le fonctionnement d’une tranche (niveaux de hiérarchisation, définition des concepts d’états, de situations, de disponibilité …)
- sur la base de l’analyse bibliographique et du méta-modèle, première proposition d’un formalisme de représentation : adaptation/évolution/enrichissement de modèles formels existants et définition des mécanismes supports à la vérification et à la simulation.
- méthodologie d’application à l’aide d’un cas d’étude « jouet » et correctifs si nécessaires,
- application sur un cas d’étude : il s’agit d’utiliser le formalisme et les moyens de vérification et de simulation proposé sur un cas d’étude fourni par EDF ; compte-tenu de la forte dimension « métier » requise pour la modélisation du cas d’étude, le travail s’effectuera en étroite collaboration avec EDF/DER.
Mots clés : Séquences de conduite, Génération, Vérification formelle, Simulation
Département(s) :
Ingénierie des Systèmes Eco-Techniques
Financement : Projet CONNEXION
Publications : hal-00779203, hal-00401680, hal-00612273    + CRAN - Publications