Explicit-state and symbolic model checking of nuclear I&C systems: A comparison

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

3 Citations (Scopus)

Abstract

In some fields of industrial automation, such as nuclear power plant (NPP) industry in Finland, thorough verification of systems and demonstration of their safety are mandatory. Model checking is one of the techniques to achieve a high level of reliability. The goal of this paper is practical: we explore which type of model checking - either explicit-state or symbolic - is more suitable to verify instrumentation and control (I&C) applications, represented as function block networks. Unlike previous studies, in addition to the common open-loop approach, which views the controller model alone, we consider closed-loop verification, where the plant is also modeled. In addition, we present a procedure to translate block networks to the language of the SPIN explicit-state model checker.
Original languageEnglish
Title of host publicationProceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society
PublisherIEEE
Pages5439-5446
Number of pages8
ISBN (Electronic)978-1-5386-1127-2
DOIs
Publication statusPublished - 18 Dec 2017
MoE publication typeA4 Article in a conference publication
EventAnnual Conference of the IEEE Industrial Electronics Society - Beijing, China
Duration: 29 Oct 20171 Nov 2017
Conference number: 43
http://iecon2017.csp.escience.cn/

Publication series

NameProceedings of the Annual Conference of the IEEE Industrial Electronics Society
PublisherIEEE
ISSN (Print)1553-572X

Conference

ConferenceAnnual Conference of the IEEE Industrial Electronics Society
Abbreviated titleIECON
CountryChina
CityBeijing
Period29/10/201701/11/2017
Internet address

Keywords

  • model cheching
  • industries
  • explosions
  • delays
  • numerical models
  • automation

Fingerprint Dive into the research topics of 'Explicit-state and symbolic model checking of nuclear I&C systems: A comparison'. Together they form a unique fingerprint.

Cite this