Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems

dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.authorPakonen, Antti
dc.contributor.authorBuzhinsky, I.
dc.contributor.authorBjörkman, K.
dc.contributor.departmentVTT Technical Research Centre of Finland
dc.contributor.departmentDepartment of Electrical Engineering and Automation
dc.date.accessioned2020-10-16T08:08:11Z
dc.date.available2020-10-16T08:08:11Z
dc.date.issued2021-01
dc.description.abstractA spurious actuation of an industrial instrumentation and control (I&C) system is a failure mode where the system or its component inadvertently produces an operation without a justified reason to do so. Design issues leading to spurious failures are difficult to analyse, but pose a high risk for safety. Model checking is a formal verification method that can be used for exhaustive analysis of I&C systems. In this paper, we explain how formal properties that address spurious failures can be specified, and how model checking can then be used to verify I&C application logic designs based on vendor-specific function block diagrams. Based on over ten years of successful practical projects in the Finnish nuclear industry, we present 21 real-world design issues (representing 37% of all detected issues), each involving a systemic failure that could lead to spurious actuation of nuclear safety I&C. We then describe how random failures of the underlying hardware architecture—another cause for spurious actuation—can also be included in the models. With an experimental evaluation based on real-world nuclear industry models, we demonstrate that our method can be effectively used for the verification of single failure tolerance.en
dc.description.versionPeer revieweden
dc.format.extent15
dc.format.mimetypeapplication/pdf
dc.identifier.citationPakonen , A , Buzhinsky , I & Björkman , K 2021 , ' Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems ' , Reliability Engineering and System Safety , vol. 205 , 107237 . https://doi.org/10.1016/j.ress.2020.107237en
dc.identifier.doi10.1016/j.ress.2020.107237
dc.identifier.issn0951-8320
dc.identifier.issn1879-0836
dc.identifier.otherPURE UUID: 37bdd88f-34e5-4eb8-996e-85cbf4c64476
dc.identifier.otherPURE ITEMURL: https://research.aalto.fi/en/publications/37bdd88f-34e5-4eb8-996e-85cbf4c64476
dc.identifier.otherPURE LINK: http://www.scopus.com/inward/record.url?scp=85091956676&partnerID=8YFLogxK
dc.identifier.otherPURE FILEURL: https://research.aalto.fi/files/52153318/ELEC_Pakonen_etal_Model_Checking_Reveals_RelEngSafSys_205_2021_finalpublishedversion.pdf
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/46953
dc.identifier.urnURN:NBN:fi:aalto-202010165850
dc.language.isoenen
dc.publisherElsevier Applied Science
dc.relation.ispartofseriesReliability Engineering and System Safetyen
dc.relation.ispartofseriesVolume 205en
dc.rightsopenAccessen
dc.subject.keywordI&c
dc.subject.keywordModel checking
dc.subject.keywordModel-based system engineering
dc.subject.keywordSpurious failure
dc.titleModel checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systemsen
dc.typeA1 Alkuperäisartikkeli tieteellisessä aikakauslehdessäfi
dc.type.versionpublishedVersion
Files