HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Theses

Strengthening fonctional validation of critical system by using Model Checking : application to Instrumentation and control systems in nuclear power plants

Abstract : 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 tje physical process and also 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.
Document type :
Theses
Complete list of metadata

https://pastel.archives-ouvertes.fr/tel-03419751
Contributor : Abes Star :  Contact
Submitted on : Monday, November 8, 2021 - 4:37:10 PM
Last modification on : Tuesday, November 9, 2021 - 3:09:20 AM
Long-term archiving on: : Wednesday, February 9, 2022 - 7:53:39 PM

File

thesisCompleteVersion_YanjunSU...
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-03419751, version 1

Citation

Yanjun Sun. Strengthening fonctional validation of critical system by using Model Checking : application to Instrumentation and control systems in nuclear power plants. Software Engineering [cs.SE]. Télécom ParisTech, 2017. English. ⟨NNT : 2017ENST0047⟩. ⟨tel-03419751⟩

Share

Metrics

Record views

26

Files downloads

5