Télécom ParisTech

Actualité

Illustration de l'actualité : PhD defense Yanjun Sun : Strengthening fonctional validation of critical system by using Model Checking: Application to Instrumentation and Control systems in nuclear power plants

PhD defense Yanjun Sun : Strengthening fonctional validation of critical system by using Model Checking: Application to Instrumentation and Control systems in nuclear power plants

lundi
9
octobre
2017

PhD Comics : I'm defending my thesis, Mom !14h30, amphi Émeraude

Jury

  • Luc COYETTE, Technical Director France Benelux, Esterel technologies/ ANSYS (Examinateur)
  • Frédéric DAUMAS, Expert Sûreté de Fonctionnement Contrôle-Commande, EDF R&D - PRISME(Examinateur)
  • Lydie DU BOUSQUET, Professeur, Université Joseph Fourier, Laboratoire d'Informatique de Grenoble (LIG) (Rapporteur)
  • Alessandro FANTECHI, Professeur, Université de Florence, Italie (Rapporteur)
  • Gérard MEMMI, Professeur, Chef du Département INFRES, Télécom ParisTech (Directeur de thèse)
  • Elie NAJM, Professeur, Télécom ParisTech (Examinateur)
  • Sylvie VIGNES, Maître de conférence, Télécom ParisTech (Directeur de thèse)

Abstract

The verication and validation of safety-critical real-time system are subject to stringent standards and certications. Recent progress in Model-Based System Engineering (MBSE) should be applied to such systems since MBSE supports early detection of defects and utilization of formal verication techniques (model checking for example). The French nuclear project "CONNEXION" proposes an innovative process introducing multi-level model-based functional validation supporting the nuclear Instrumentation and Control (I&C) system development life cycle. Various modeling and verication tools provided by project partners automate this process as much as possible. "CONNEXION" also proposes a verication platform integrating model-based design and simulation of the nuclear I&C system.

As part of the "CONNEXION" project, this thesis proposes a model-based testing methodology to reinforce functional validation of the I&C systems. The methodology focus on an iterative use of a model checker to generate structural coverage-based test sequence. We also proposes a refinement technique of progressively adding environment constraints during test generation. The refinement is expected to support the passage from structural coverage-based test sequence to functional requirements-based test case. The methodology also considers the state explosion problem of a model checker and proposes a heuristic called hybrid verication combining model checking and simulation. The methodology has been partly tested on an industrial case study, with support of "CONNEXION" tools.