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
Explicit-state and symbolic model checking of nuclear I&C systems: A comparison
Department of Electrical Engineering and Automation, Aalto University.
VTT Technical Research Centre of Finland, Espoo.
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering, Computer Science. Department of Electrical Engineering and Automation, Aalto University.ORCID iD: 0000-0002-9315-9920
2017 (English)In: Proceedings IECON 2017: 43rd Annual Conference of the IEEE Industrial Electronics Society, Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2017, p. 5439-5446Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Piscataway, NJ: Institute of Electrical and Electronics Engineers (IEEE), 2017. p. 5439-5446
Series
IEEE Industrial Electronics Society, ISSN 1553-572X
National Category
Computer Systems
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-68268DOI: 10.1109/IECON.2017.8216942ISI: 000427164805061Scopus ID: 2-s2.0-85046626566ISBN: 9781538611272 (electronic)OAI: oai:DiVA.org:ltu-68268DiVA, id: diva2:1196479
Conference
43rd Annual Conference of the IEEE Industrial Electronics Society, IECON 2017, Bejing, China, 29 October - 1 November 2017
Available from: 2018-04-10 Created: 2018-04-10 Last updated: 2018-05-22Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Vyatkin, Valeriy
By organisation
Computer Science
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
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