Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions
Loading...
Access rights
openAccess
publishedVersion
URL
Journal Title
Journal ISSN
Volume Title
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
Authors
Date
2019
Major/Subject
Mcode
Degree programme
Language
en
Pages
18
Series
IEEE Access, Volume 7, pp. 162139-162156
Abstract
Model checking has been successfully used for detailed formal verification of instrumentation and control (IC) 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 IC 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 an approach to model and formally verify protection functions allocated to one or several IC systems, accounting for hardware component failures and delays in communication within and between the systems. Formal verification is done with model checking, whose feasibility on such complex systems is achieved by utilizing the symmetry of IC systems: The components of the overall model that do not influence the checked requirements are eliminated, and the failing components are fixed. Generation of such abstracted models, as well as subsequent verification of their requirements and symmetry with the NuSMV symbolic model checker, is handled by a software tool. In addition, we explore how to specify formal requirements for systems of the considered class. Based on a case study built around a semi-fictitious nuclear power plant protection system that achieves reliability by means of redundancy, we demonstrate how failure tolerance of even detailed system designs can be formally verified.Description
Keywords
Fault tolerance, Formal verification, Model checking, Nuclear IC systems
Other note
Citation
Buzhinsky, I & Pakonen, A 2019, ' Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions ', IEEE Access, vol. 7, 8892461, pp. 162139-162156 . https://doi.org/10.1109/ACCESS.2019.2951938