Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions
Model checking has been successfully used for detailed formal verification of instrumentation and control (I&C) 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 I&C har...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2019-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/8892461/ |
| _version_ | 1818910078033461248 |
|---|---|
| author | Igor Buzhinsky Antti Pakonen |
| author_facet | Igor Buzhinsky Antti Pakonen |
| author_sort | Igor Buzhinsky |
| collection | DOAJ |
| description | Model checking has been successfully used for detailed formal verification of instrumentation and control (I&C) 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 I&C 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 I&C 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 I&C 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. |
| first_indexed | 2024-12-19T22:37:05Z |
| format | Article |
| id | doaj.art-c79bec426d084eee8f3fe3c47c1ae3ac |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-19T22:37:05Z |
| publishDate | 2019-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-c79bec426d084eee8f3fe3c47c1ae3ac2022-12-21T20:03:11ZengIEEEIEEE Access2169-35362019-01-01716213916215610.1109/ACCESS.2019.29519388892461Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety FunctionsIgor Buzhinsky0https://orcid.org/0000-0003-3713-6051Antti Pakonen1https://orcid.org/0000-0002-6803-2303Department of Electrical Engineering and Automation, Aalto University, Espoo, FinlandVTT Technical Research Centre of Finland, Espoo, FinlandModel checking has been successfully used for detailed formal verification of instrumentation and control (I&C) 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 I&C 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 I&C 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 I&C 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.https://ieeexplore.ieee.org/document/8892461/Formal verificationmodel checkingnuclear I&C systemsfault tolerance |
| spellingShingle | Igor Buzhinsky Antti Pakonen Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions IEEE Access Formal verification model checking nuclear I&C systems fault tolerance |
| title | Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions |
| title_full | Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions |
| title_fullStr | Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions |
| title_full_unstemmed | Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions |
| title_short | Model-Checking Detailed Fault-Tolerant Nuclear Power Plant Safety Functions |
| title_sort | model checking detailed fault tolerant nuclear power plant safety functions |
| topic | Formal verification model checking nuclear I&C systems fault tolerance |
| url | https://ieeexplore.ieee.org/document/8892461/ |
| work_keys_str_mv | AT igorbuzhinsky modelcheckingdetailedfaulttolerantnuclearpowerplantsafetyfunctions AT anttipakonen modelcheckingdetailedfaulttolerantnuclearpowerplantsafetyfunctions |