Model Checking of Safety-Critical Software in the Nuclear Engineering Domain (2012)

AUTHORS:

Lahtinen Jussi , Valkonen Janne , Björkman Kim , Frits Juho , Niemelä Ilkka , Heljanko Keijo

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 nuclearengineering. It puts forward modelchecking, 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 safetycritical systems in the nucleardomain. 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 modelchecking process.

URL:
http://dx.doi.org/10.1016/j.ress.2012.03.021

@article{
    LahValBjo12_ini,
    author = {Lahtinen, Jussi and Valkonen, Janne and Björkman, Kim and Frits, Juho and Niemel{\"a}, Ilkka and Heljanko, Keijo},
    volume = "105",
    note = "",
    responsibleauthor = "Ilkka Niemelä, Keijo Heljanko",
    language = "eng",
    title = "Model Checking of Safety-Critical Software in the Nuclear Engineering Domain",
    ee = "http://dx.doi.org/10.1016/j.ress.2012.03.021",
    journal = "Reliability Engineering \& System Safety (RESS)",
    issn = "0951-8320",
    number = "0",
    pages = "104-113",
    juforank = "2",
    url = "http://dx.doi.org/10.1016/j.ress.2012.03.021",
    corerank = "NA",
    flags = "copy DC",
    il = "no",
    year = "2012",
    keywords = "model checking, verification, safety, I\&C, automation, nuclear",
    unitcode = "T306-99,T312-1",
    impactfactor = "A1",
    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 nuclearengineering. It puts forward modelchecking, 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 safetycritical systems in the nucleardomain. 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 modelchecking process."
}

AUTHORS:

ABSTRACT:

URL: http://dx.doi.org/10.1016/j.ress.2012.03.021

URL:
http://dx.doi.org/10.1016/j.ress.2012.03.021