Learning Centre

Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Buzhinsky, Igor
dc.contributor.author Pakonen, Antti
dc.date.accessioned 2021-01-25T10:11:59Z
dc.date.available 2021-01-25T10:11:59Z
dc.date.issued 2019
dc.identifier.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 en
dc.identifier.issn 2169-3536
dc.identifier.other PURE UUID: 56f8705a-a850-4e05-ba05-af1c93324c6d
dc.identifier.other PURE ITEMURL: https://research.aalto.fi/en/publications/56f8705a-a850-4e05-ba05-af1c93324c6d
dc.identifier.other PURE LINK: http://www.scopus.com/inward/record.url?scp=85077964576&partnerID=8YFLogxK
dc.identifier.other PURE FILEURL: https://research.aalto.fi/files/54914715/ELEC_Buzhinsky_etal_Model_Checking_IEEEAccess_2019_finalpublishedversion.pdf
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/102152
dc.description.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. en
dc.format.extent 18
dc.format.extent 162139-162156
dc.format.mimetype application/pdf
dc.language.iso en en
dc.relation.ispartofseries IEEE Access en
dc.relation.ispartofseries Volume 7 en
dc.rights openAccess en
dc.title Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions en
dc.type A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä fi
dc.description.version Peer reviewed en
dc.contributor.department Department of Electrical Engineering and Automation
dc.contributor.department VTT Technical Research Centre of Finland
dc.subject.keyword Fault tolerance
dc.subject.keyword Formal verification
dc.subject.keyword Model checking
dc.subject.keyword Nuclear IC systems
dc.identifier.urn URN:NBN:fi:aalto-202101251462
dc.identifier.doi 10.1109/ACCESS.2019.2951938
dc.type.version publishedVersion

Files in this item

Files Size Format View

There are no open access files associated with this item.

This item appears in the following Collection(s)

Show simple item record

Search archive

Advanced Search

article-iconSubmit a publication