aalto1 untyped-item.component.html
Symmetry Breaking in Model Checking of Fault-Tolerant Nuclear Instrumentation and Control Systems
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)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Authors
Date
Major/Subject
Mcode
Degree programme
Language
en
Pages
11
Series
IEEE Access, Volume 8, pp. 197684-197694
Abstract
One of the approaches to assure reliability of nuclear instrumentation and control (I&C) systems is model checking, a formal verification technique. Model checking is computationally demanding, but nuclear I&C systems have certain properties that simplify the verification problem. The most notable of these properties are redundancy (duplication of certain system parts in several divisions) and symmetry, which are the means of ensuring failure tolerance. In this work, we extend our previous method of model checking failure tolerance of nuclear I&C systems by proposing an automated symmetry breaking approach that utilizes these properties to simplify the verification problem. As a result, fewer failure combinations need to be checked. We evaluate this approach on a case study that encompasses three safety functions allocated to four I&C systems in the same I&C model.
Description
Other note
Citation
Buzhinsky, I & Pakonen, A 2020, 'Symmetry Breaking in Model Checking of Fault-Tolerant Nuclear Instrumentation and Control Systems', IEEE Access, vol. 8, pp. 197684-197694. https://doi.org/10.1109/ACCESS.2020.3034799