14h30, amphi Émeraude
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.