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

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.authorBuzhinsky, Igor
dc.contributor.authorPakonen, Antti
dc.contributor.departmentDepartment of Electrical Engineering and Automation
dc.contributor.departmentVTT Technical Research Centre of Finland
dc.date.accessioned2021-01-25T10:11:59Z
dc.date.available2021-01-25T10:11:59Z
dc.date.issued2019
dc.description.abstractModel 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.description.versionPeer revieweden
dc.format.extent18
dc.format.extent162139-162156
dc.format.mimetypeapplication/pdf
dc.identifier.citationBuzhinsky , 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.2951938en
dc.identifier.doi10.1109/ACCESS.2019.2951938
dc.identifier.issn2169-3536
dc.identifier.otherPURE UUID: 56f8705a-a850-4e05-ba05-af1c93324c6d
dc.identifier.otherPURE ITEMURL: https://research.aalto.fi/en/publications/56f8705a-a850-4e05-ba05-af1c93324c6d
dc.identifier.otherPURE LINK: http://www.scopus.com/inward/record.url?scp=85077964576&partnerID=8YFLogxK
dc.identifier.otherPURE FILEURL: https://research.aalto.fi/files/54914715/ELEC_Buzhinsky_etal_Model_Checking_IEEEAccess_2019_finalpublishedversion.pdf
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/102152
dc.identifier.urnURN:NBN:fi:aalto-202101251462
dc.language.isoenen
dc.publisherIEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
dc.relation.ispartofseriesIEEE Accessen
dc.relation.ispartofseriesVolume 7en
dc.rightsopenAccessen
dc.subject.keywordFault tolerance
dc.subject.keywordFormal verification
dc.subject.keywordModel checking
dc.subject.keywordNuclear IC systems
dc.titleModel-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functionsen
dc.typeA1 Alkuperäisartikkeli tieteellisessä aikakauslehdessäfi
dc.type.versionpublishedVersion
Files