Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal Verification of Safety I&C System Designs: Two Nuclear Power Plant Related Applications
Show others and affiliations
2008 (English)In: Proceedings Man-Technology-Organisation Session, Enlarged Halden Programme Group Meeting, Norway: Institt for energiteknikk , 2008Conference paper, Published paper (Other academic)
Abstract [en]

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.

Place, publisher, year, edition, pages
Norway: Institt for energiteknikk , 2008.
National Category
Philosophy
Identifiers
URN: urn:nbn:se:kth:diva-90777OAI: oai:DiVA.org:kth-90777DiVA: diva2:506532
Conference
Enlarged Halden Programme Group Meeting. Proc. Man-Technology-Organisation Session. Loen, Norway. 18–23 May 2008
Note
QC 20120508Available from: 2012-02-28 Created: 2012-02-28 Last updated: 2012-05-08Bibliographically approved

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Holmberg, Jan-Erik
Philosophy

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 31 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf