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

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
Date
2021-01
Major/Subject
Mcode
Degree programme
Language
en
Pages
15
Series
Reliability Engineering and System Safety, Volume 205
Abstract
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.
Description
Keywords
I&c, Model checking, Model-based system engineering, Spurious failure
Other note
Citation
Pakonen , A , 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 , vol. 205 , 107237 . https://doi.org/10.1016/j.ress.2020.107237