| 1. |
- Valkonen, J., et al.
(författare)
-
Formal Verification of Safety I&C System Designs : Two Nuclear Power Plant Related Applications
- 2008
-
Ingår i: Proceedings Man-Technology-Organisation Session, Enlarged Halden Programme Group Meeting. - Norway : Institt for energiteknikk.
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- Instrumentation and control (I&C) systems play a crucial role in the operation of nuclear power plants(NPP) and other safety critical processes. An important change is the replacement of the old analogue I&Csystems with new digitalised ones. The programmable digital logic controllers enable more complicatedcontrol tasks than the old analogue systems and thus the validation of the control logic designs against safetyrequirements has become more important. In order to diminish the subjective component of the evaluationthere is a need to develop new formal verification methods. A promising approach is a method called modelchecking, which enables the complete verification of requirements when a finite state machine model of thesystem is available. The use of model checking to verify two nuclear power plant related systems isdescribed: an arc protection system and a reactor emergency cooling system. For the verification, it was alsonecessary to model the operation environment of the device and the larger system it is part of. Theenvironment models could be kept relatively simple, but it is important that the essential behaviour of theenvironment is covered. The reactor emergency cooling system is in use in an operating nuclear power plantand the arc protection system model included a typical realistic operation environment. The results showedthat it was possible to reliably verify the presence of desired behaviour as well as the absence of anundesired behaviour of the system. The possibility for complete verification makes model checking differentfrom simulation-based testing where only a number of selected scenarios can be simulated and one can neverbe sure that all the possible behaviour is covered. The challenges for future research are to develop morededicated methods for the verification of safety critical automation and safety critical embedded software.
|
|
| 2. |
- Valkonen, J., et al.
(författare)
-
Model-Based Analysis of an Arc Protection and an Emergency Cooling System
- 2008
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Instrumentation and control (I&C) systems play a crucial role in the operation of nuclearpower plants and other safety critical processes. An important change that will be going on inthe near future is the replacement of the old analogue I&C systems by new digitalised ones.The programmable digital logic controllers enable more complicated control tasks than the oldanalogue systems and thus the verification of the control logic designs against safetyrequirements has become more important. In order to diminish the subjective component ofthe evaluation, there is a need to develop new formal verification methods.This report summarizes the work done in the MODSAFE 2007 project on two case studieswhere model checking techniques have been used to study an arc protection system and anemergency cooling system. Model checking tools offer typically a finite state machine basedmodelling language for modelling the system to be verified, a specification language(temporal logic) for expressing the properties to be verified and a set of analysis tools to checkthat the system satisfies the given properties. A state of the art open source model checkingsystem NuSMV was employed and using a reasonable effort it was possible to (i) model bothsystems on an adequate level, (ii) to formulate required safety properties in the specificationlanguage, and (iii) to perform a full verification of the properties using the NuSMV system.This indicates that current model checking techniques are applicable in the analysis of safetyI&C systems in NPPs.
|
|
