Symmetry Breaking in Model Checking of Fault-Tolerant Nuclear Instrumentation and Control Systems

Thumbnail Image

Access rights

openAccess

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)

Authors

Date

2020

Department

Department of Electrical Engineering and Automation

Major/Subject

Mcode

Degree programme

Language

en

Pages

11
197684-197694

Series

IEEE Access, Volume 8

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

Keywords

Model checking, Input variables, Safety, Instruments, Control systems, Fault tolerance, Fault tolerant systems, Formal verification, model checking, symmetry breaking, nuclear I&amp, C systems, fault tolerance, SOFTWARE

Other note

DOI

10.1109/ACCESS.2020.3034799

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

Permanent link to this item

https://urn.fi/URN:NBN:fi:aalto-202101251585

Collections

[article-cris] Sähkötekniikan korkeakoulu / ELEC