IDEAS home Printed from https://ideas.repec.org/a/eee/reensy/v105y2012icp104-113.html
   My bibliography  Save this article

Model checking of safety-critical software in the nuclear engineering domain

Author

Listed:
  • Lahtinen, J.
  • Valkonen, J.
  • Björkman, K.
  • Frits, J.
  • Niemelä, I.
  • Heljanko, K.

Abstract

Instrumentation and control (I&C) systems play a vital role in the operation of safety-critical processes. Digital programmable logic controllers (PLC) enable sophisticated control tasks which sets high requirements for system validation and verification methods. Testing and simulation have an important role in the overall verification of a system but are not suitable for comprehensive evaluation because only a limited number of system behaviors can be analyzed due to time limitations. Testing is also performed too late in the development lifecycle and thus the correction of design errors is expensive. This paper discusses the role of formal methods in software development in the area of nuclear engineering. It puts forward model checking, a computer-aided formal method for verifying the correctness of a system design model, as a promising approach to system verification. The main contribution of the paper is the development of systematic methodology for modeling safety critical systems in the nuclear domain. Two case studies are reviewed, in which we have found errors that were previously not detected. We also discuss the actions that should be taken in order to increase confidence in the model checking process.

Suggested Citation

  • Lahtinen, J. & Valkonen, J. & Björkman, K. & Frits, J. & Niemelä, I. & Heljanko, K., 2012. "Model checking of safety-critical software in the nuclear engineering domain," Reliability Engineering and System Safety, Elsevier, vol. 105(C), pages 104-113.
    • Handle: RePEc:eee:reensy:v:105:y:2012:i:c:p:104-113
    DOI: 10.1016/j.ress.2012.03.021
    as

    Download full text from publisher

    File URL: http://www.sciencedirect.com/science/article/pii/S0951832012000555
    Download Restriction: Full text for ScienceDirect subscribers only
    File URL: https://libkey.io/10.1016/j.ress.2012.03.021?utm_source=ideas
    LibKey link: if access is restricted and if your library uses this service, LibKey will redirect you to where you can use your library subscription to access this item
    ---><---

    As the access to this document is restricted, you may want to search for a different version of it.

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. Lahtinen, Jussi & Kuismin, Tuomas & Heljanko, Keijo, 2015. "Verifying large modular systems using iterative abstraction refinement," Reliability Engineering and System Safety, Elsevier, vol. 139(C), pages 120-130.
    2. Cheng, Ruijun & Cheng, Yu & Chen, Dewang & Song, Haifeng, 2021. "Online quantitative safety monitoring approach for unattended train operation system considering stochastic factors," Reliability Engineering and System Safety, Elsevier, vol. 216(C).
    3. Pakonen, Antti & Buzhinsky, I & Björkman, K, 2021. "Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems," Reliability Engineering and System Safety, Elsevier, vol. 205(C).
    4. Cheng, Ruijun & Zhou, Jin & Chen, Dewang & Song, Yongduan, 2016. "Model-based verification method for solving the parameter uncertainty in the train control system," Reliability Engineering and System Safety, Elsevier, vol. 145(C), pages 169-182.
    5. Gouyon, David & Pétin, Jean-François & Cochard, Thomas & Devic, Catherine, 2020. "Architecture assessment for safety critical plant operation using reachability analysis of timed automata," Reliability Engineering and System Safety, Elsevier, vol. 199(C).

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:eee:reensy:v:105:y:2012:i:c:p:104-113. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    We have no bibliographic references for this item. You can help adding them by using this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Catherine Liu (email available below). General contact details of provider: https://www.journals.elsevier.com/reliability-engineering-and-system-safety .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.