Verification of fault tolerant safety I&C systems using model checking

Antti Pakonen; Igor Buzhinsky

doi:10.1109/ICIT.2019.8755014

Verification of fault tolerant safety I&C systems using model checking

Antti Pakonen
, Igor Buzhinsky

Research output: Chapter in Book/Report/Conference proceeding › Conference article in proceedings › Scientific › peer-review

7 Citations (Scopus)

Abstract

Model checking has been successfully used for detailed formal verification of instrumentation and control (I&C) systems, as long as the focus has been on the application logic, alone. In safety-critical applications, fault tolerance is also an important aspect, but introducing I&C hardware failure modes to the formal models comes at a significant computational cost. Previous attempts have led to state space explosion, and prohibitively long processing times. In this paper, we present a method for adding hardware component failures and communication delays into I&C application logic models for the NuSMV symbolic model checker. Based on a case study built around a semi-fictitious, four-redundant nuclear power plant protection system, we demonstrate how even detailed system designs can be verified, if the focus is kept on single failure tolerance.

Original language	English
Title of host publication	Proceedings of the 20th IEEE International Conference on Industrial Technology, ICIT 2019
Publisher	IEEE
Pages	969-974
Number of pages	6
ISBN (Electronic)	9781538663769
DOIs	https://doi.org/10.1109/ICIT.2019.8755014
Publication status	Published - 1 Feb 2019
MoE publication type	A4 Conference publication
Event	IEEE International Conference on Industrial Technology - Melbourne, Australia Duration: 13 Feb 2019 → 15 Feb 2019

Publication series

Name	Proceedings of the IEEE International Conference on Industrial Technology
Volume	2019-February
ISSN (Print)	2641-0184
ISSN (Electronic)	2643-2978

Conference

Conference	IEEE International Conference on Industrial Technology
Abbreviated title	ICIT
Country/Territory	Australia
City	Melbourne
Period	13/02/2019 → 15/02/2019

Funding

ACKNOWLEDGMENT This work has been funded by the Finnish Research Programme on Nuclear Power Plant Safety 2015-2018 (SAFIR 2018), and by the Government of the Russian Federation (Grant 08-08).

Keywords

Fault tolerance
Formal verification
Model checking

Access to Document

10.1109/ICIT.2019.8755014

https://cris.vtt.fi/en/publications/verification-of-fault-tolerant-safety-iampc-systems-using-model-c-2

Cite this

Pakonen, A., & Buzhinsky, I. (2019). Verification of fault tolerant safety I&C systems using model checking. In Proceedings of the 20th IEEE International Conference on Industrial Technology, ICIT 2019 (pp. 969-974). Article 8755014 (Proceedings of the IEEE International Conference on Industrial Technology; Vol. 2019-February). IEEE. https://doi.org/10.1109/ICIT.2019.8755014

@inproceedings{c888e8a850eb4db4a8c48b8188918bb4,

title = "Verification of fault tolerant safety I\&C systems using model checking",

abstract = "Model checking has been successfully used for detailed formal verification of instrumentation and control (I\&C) systems, as long as the focus has been on the application logic, alone. In safety-critical applications, fault tolerance is also an important aspect, but introducing I\&C hardware failure modes to the formal models comes at a significant computational cost. Previous attempts have led to state space explosion, and prohibitively long processing times. In this paper, we present a method for adding hardware component failures and communication delays into I\&C application logic models for the NuSMV symbolic model checker. Based on a case study built around a semi-fictitious, four-redundant nuclear power plant protection system, we demonstrate how even detailed system designs can be verified, if the focus is kept on single failure tolerance.",

keywords = "Fault tolerance, Formal verification, Model checking",

author = "Antti Pakonen and Igor Buzhinsky",

year = "2019",

month = feb,

day = "1",

doi = "10.1109/ICIT.2019.8755014",

language = "English",

series = "Proceedings of the IEEE International Conference on Industrial Technology",

publisher = "IEEE",

pages = "969--974",

booktitle = "Proceedings of the 20th IEEE International Conference on Industrial Technology, ICIT 2019",

address = "United States",

note = "IEEE International Conference on Industrial Technology, ICIT ; Conference date: 13-02-2019 Through 15-02-2019",

}

Pakonen, A & Buzhinsky, I 2019, Verification of fault tolerant safety I&C systems using model checking. in Proceedings of the 20th IEEE International Conference on Industrial Technology, ICIT 2019., 8755014, Proceedings of the IEEE International Conference on Industrial Technology, vol. 2019-February, IEEE, pp. 969-974, IEEE International Conference on Industrial Technology, Melbourne, Australia, 13/02/2019. https://doi.org/10.1109/ICIT.2019.8755014

Verification of fault tolerant safety I&C systems using model checking. / Pakonen, Antti; Buzhinsky, Igor.
Proceedings of the 20th IEEE International Conference on Industrial Technology, ICIT 2019. IEEE, 2019. p. 969-974 8755014 (Proceedings of the IEEE International Conference on Industrial Technology; Vol. 2019-February).

Research output: Chapter in Book/Report/Conference proceeding › Conference article in proceedings › Scientific › peer-review

TY - GEN

T1 - Verification of fault tolerant safety I&C systems using model checking

AU - Pakonen, Antti

AU - Buzhinsky, Igor

PY - 2019/2/1

Y1 - 2019/2/1

N2 - Model checking has been successfully used for detailed formal verification of instrumentation and control (I&C) systems, as long as the focus has been on the application logic, alone. In safety-critical applications, fault tolerance is also an important aspect, but introducing I&C hardware failure modes to the formal models comes at a significant computational cost. Previous attempts have led to state space explosion, and prohibitively long processing times. In this paper, we present a method for adding hardware component failures and communication delays into I&C application logic models for the NuSMV symbolic model checker. Based on a case study built around a semi-fictitious, four-redundant nuclear power plant protection system, we demonstrate how even detailed system designs can be verified, if the focus is kept on single failure tolerance.

AB - Model checking has been successfully used for detailed formal verification of instrumentation and control (I&C) systems, as long as the focus has been on the application logic, alone. In safety-critical applications, fault tolerance is also an important aspect, but introducing I&C hardware failure modes to the formal models comes at a significant computational cost. Previous attempts have led to state space explosion, and prohibitively long processing times. In this paper, we present a method for adding hardware component failures and communication delays into I&C application logic models for the NuSMV symbolic model checker. Based on a case study built around a semi-fictitious, four-redundant nuclear power plant protection system, we demonstrate how even detailed system designs can be verified, if the focus is kept on single failure tolerance.

KW - Fault tolerance

KW - Formal verification

KW - Model checking

UR - https://www.scopus.com/pages/publications/85069054364

U2 - 10.1109/ICIT.2019.8755014

DO - 10.1109/ICIT.2019.8755014

M3 - Conference article in proceedings

AN - SCOPUS:85069054364

T3 - Proceedings of the IEEE International Conference on Industrial Technology

SP - 969

EP - 974

BT - Proceedings of the 20th IEEE International Conference on Industrial Technology, ICIT 2019

PB - IEEE

T2 - IEEE International Conference on Industrial Technology

Y2 - 13 February 2019 through 15 February 2019

ER -

Verification of fault tolerant safety I&C systems using model checking

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this