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

Igor Buzhinskii; Antti Pakonen; Valeriy Vyatkin

doi:10.1109/IECON.2017.8216942

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

Igor Buzhinskii, Antti Pakonen, Valeriy Vyatkin

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference article in proceedings › Scientific › vertaisarvioitu

11 Sitaatiot (Scopus)

Abstrakti

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.

Alkuperäiskieli	Englanti
Otsikko	Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society
Kustantaja	IEEE
Sivut	5439-5446
Sivumäärä	8
ISBN (elektroninen)	978-1-5386-1127-2
DOI - pysyväislinkit	https://doi.org/10.1109/IECON.2017.8216942
Tila	Julkaistu - 18 jouluk. 2017
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisussa
Tapahtuma	Annual Conference of the IEEE Industrial Electronics Society - Beijing, Kiina Kesto: 29 lokak. 2017 → 1 marrask. 2017 Konferenssinumero: 43 http://iecon2017.csp.escience.cn/

Julkaisusarja

Nimi	Proceedings of the Annual Conference of the IEEE Industrial Electronics Society
Kustantaja	IEEE
ISSN (painettu)	1553-572X

Conference

Conference	Annual Conference of the IEEE Industrial Electronics Society
Lyhennettä	IECON
Maa/Alue	Kiina
Kaupunki	Beijing
Ajanjakso	29/10/2017 → 01/11/2017
www-osoite	http://iecon2017.csp.escience.cn/

Pääsy asiakirjaan

10.1109/IECON.2017.8216942

Siteeraa tätä

Buzhinskii, I., Pakonen, A., & Vyatkin, V. (2017). Explicit-state and symbolic model checking of nuclear I&C systems: A comparison. teoksessa Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society (Sivut 5439-5446). (Proceedings of the Annual Conference of the IEEE Industrial Electronics Society). IEEE. https://doi.org/10.1109/IECON.2017.8216942

@inproceedings{6d618c9498a24e5dace8c54bc8951c12,

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

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.",

keywords = "model cheching, industries, explosions, delays, numerical models, automation",

author = "Igor Buzhinskii and Antti Pakonen and Valeriy Vyatkin",

year = "2017",

month = dec,

day = "18",

doi = "10.1109/IECON.2017.8216942",

language = "English",

series = "Proceedings of the Annual Conference of the IEEE Industrial Electronics Society",

publisher = "IEEE",

pages = "5439--5446",

booktitle = "Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society",

address = "United States",

note = "Annual Conference of the IEEE Industrial Electronics Society, IECON ; Conference date: 29-10-2017 Through 01-11-2017",

url = "http://iecon2017.csp.escience.cn/",

}

Buzhinskii, I, Pakonen, A & Vyatkin, V 2017, Explicit-state and symbolic model checking of nuclear I&C systems: A comparison. julkaisussa Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society. Proceedings of the Annual Conference of the IEEE Industrial Electronics Society, IEEE, Sivut 5439-5446, Annual Conference of the IEEE Industrial Electronics Society, Beijing, Kiina, 29/10/2017. https://doi.org/10.1109/IECON.2017.8216942

Explicit-state and symbolic model checking of nuclear I&C systems: A comparison. / Buzhinskii, Igor; Pakonen, Antti; Vyatkin, Valeriy.
Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society. IEEE, 2017. s. 5439-5446 (Proceedings of the Annual Conference of the IEEE Industrial Electronics Society).

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussa › Conference article in proceedings › Scientific › vertaisarvioitu

TY - GEN

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

AU - Buzhinskii, Igor

AU - Pakonen, Antti

AU - Vyatkin, Valeriy

N1 - Conference code: 43

PY - 2017/12/18

Y1 - 2017/12/18

N2 - 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.

AB - 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.

KW - model cheching

KW - industries

KW - explosions

KW - delays

KW - numerical models

KW - automation

U2 - 10.1109/IECON.2017.8216942

DO - 10.1109/IECON.2017.8216942

M3 - Conference article in proceedings

T3 - Proceedings of the Annual Conference of the IEEE Industrial Electronics Society

SP - 5439

EP - 5446

BT - Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society

PB - IEEE

T2 - Annual Conference of the IEEE Industrial Electronics Society

Y2 - 29 October 2017 through 1 November 2017

ER -

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

Abstrakti

Julkaisusarja

Conference

Pääsy asiakirjaan

Sormenjälki

Siteeraa tätä