Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems

Antti Pakonen*, I. Buzhinsky, K. Björkman

*Tämän työn vastaava kirjoittaja

Tutkimustuotos: LehtiartikkeliArticleScientificvertaisarvioitu

2 Sitaatiot (Scopus)
38 Lataukset (Pure)

Abstrakti

A spurious actuation of an industrial instrumentation and control (I&C) system is a failure mode where the system or its component inadvertently produces an operation without a justified reason to do so. Design issues leading to spurious failures are difficult to analyse, but pose a high risk for safety. Model checking is a formal verification method that can be used for exhaustive analysis of I&C systems. In this paper, we explain how formal properties that address spurious failures can be specified, and how model checking can then be used to verify I&C application logic designs based on vendor-specific function block diagrams. Based on over ten years of successful practical projects in the Finnish nuclear industry, we present 21 real-world design issues (representing 37% of all detected issues), each involving a systemic failure that could lead to spurious actuation of nuclear safety I&C. We then describe how random failures of the underlying hardware architecture—another cause for spurious actuation—can also be included in the models. With an experimental evaluation based on real-world nuclear industry models, we demonstrate that our method can be effectively used for the verification of single failure tolerance.

AlkuperäiskieliEnglanti
Artikkeli107237
Sivumäärä15
JulkaisuReliability Engineering and System Safety
Vuosikerta205
DOI - pysyväislinkit
TilaJulkaistu - tammikuuta 2021
OKM-julkaisutyyppiA1 Julkaistu artikkeli, soviteltu

Sormenjälki Sukella tutkimusaiheisiin 'Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä