Strengthening functional validation of critical system by using Model Checking: Application to Instrumentation and Control systems in nuclear power plants

The verification and validation of safety-critical real-time system are subject to stringent standards and certifications. Recent progress in model-based system engineering should be applied to such systems since it allows early detection of defects and formal verification techniques. This thesis proposes a model-based testing (MBT) methodology dedicated to functional validation of safety-critical real-time systems. The method is directed by the structural coverage of the Lustre model co-simulated with the physical process and by the functional requirements. It relies on a repetitive use of a model checker to generate coverage-based open-loop test sequences. We also propose a refinement technique of progressively adding environment constraints during test generation. The refinement is expected to support the passage from coverage-based open-loop test sequence to functional requirements-based closed-loop test case. Our methodology also considers the state explosion problem of a model checker and proposes a heuristic called hybrid verification combining model checking and simulation. (author)