Scalable methods of discrete plant model generation for closed-loop model checking

Igor Buzhinskii; Antti Pakonen; Valeriy Vyatkin

doi:10.1109/IECON.2017.8216949

Scalable methods of discrete plant model generation for closed-loop model checking

Igor Buzhinskii, Antti Pakonen, Valeriy Vyatkin

Research output: Chapter in Book/Report/Conference proceeding › Conference article in proceedings › Scientific › peer-review

257 Downloads (Pure)

Abstract

To facilitate correctness and safety of mission-critical automation systems, formal methods should be applied in addition to simulation and testing. One of such formal methods is model checking, which is capable of verifying complex requirements for the system's model. If both the controller and the controlled plant are formally modeled, then the variant of this technique called closed-loop model checking can be applied. Recently, a technique of automatic plant model generation has been proposed which is applicable in this scenario. This paper continues the work in this direction by presenting two plant model construction approaches which are much more scalable with respect to the previous one, and puts this work into a more practical context. The approaches are evaluated on a case study from the nuclear automation domain.

Original language	English
Title of host publication	Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society
Publisher	IEEE
Pages	5483-5488
Number of pages	6
ISBN (Electronic)	978-1-5386-1127-2
DOIs	https://doi.org/10.1109/IECON.2017.8216949
Publication status	Published - 18 Dec 2017
MoE publication type	A4 Conference publication
Event	Annual Conference of the IEEE Industrial Electronics Society - Beijing, China Duration: 29 Oct 2017 → 1 Nov 2017 Conference number: 43 http://iecon2017.csp.escience.cn/

Publication series

Name	Proceedings of the Annual Conference of the IEEE Industrial Electronics Society
Publisher	IEEE
ISSN (Print)	1553-572X

Conference

Conference	Annual Conference of the IEEE Industrial Electronics Society
Abbreviated title	IECON
Country/Territory	China
City	Beijing
Period	29/10/2017 → 01/11/2017
Internet address	http://iecon2017.csp.escience.cn/

Keywords

model checking
solid modeling
automation
computational modeling
context modeling
data models
tools

Access to Document

10.1109/IECON.2017.8216949

ELEC_Buzhinsky_etal_Scalable-Methods-of-Discrete_IECON_2017_acceptedAccepted author manuscript, 223 KB

Cite this

Buzhinskii, I., Pakonen, A., & Vyatkin, V. (2017). Scalable methods of discrete plant model generation for closed-loop model checking. In Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society (pp. 5483-5488). (Proceedings of the Annual Conference of the IEEE Industrial Electronics Society). IEEE. https://doi.org/10.1109/IECON.2017.8216949

@inproceedings{c2c5d86fdd9444859d0c3b096d0bf117,

title = "Scalable methods of discrete plant model generation for closed-loop model checking",

abstract = "To facilitate correctness and safety of mission-critical automation systems, formal methods should be applied in addition to simulation and testing. One of such formal methods is model checking, which is capable of verifying complex requirements for the system's model. If both the controller and the controlled plant are formally modeled, then the variant of this technique called closed-loop model checking can be applied. Recently, a technique of automatic plant model generation has been proposed which is applicable in this scenario. This paper continues the work in this direction by presenting two plant model construction approaches which are much more scalable with respect to the previous one, and puts this work into a more practical context. The approaches are evaluated on a case study from the nuclear automation domain.",

keywords = "model checking, solid modeling, automation, computational modeling, context modeling, data models, tools",

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

year = "2017",

month = dec,

day = "18",

doi = "10.1109/IECON.2017.8216949",

language = "English",

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

publisher = "IEEE",

pages = "5483--5488",

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, Scalable methods of discrete plant model generation for closed-loop model checking. in Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society. Proceedings of the Annual Conference of the IEEE Industrial Electronics Society, IEEE, pp. 5483-5488, Annual Conference of the IEEE Industrial Electronics Society, Beijing, China, 29/10/2017. https://doi.org/10.1109/IECON.2017.8216949

Scalable methods of discrete plant model generation for closed-loop model checking. / Buzhinskii, Igor; Pakonen, Antti; Vyatkin, Valeriy.
Proceedings IECON 2017 - 43rd Annual Conference of the IEEE Industrial Electronics Society. IEEE, 2017. p. 5483-5488 (Proceedings of the Annual Conference of the IEEE Industrial Electronics Society).

Research output: Chapter in Book/Report/Conference proceeding › Conference article in proceedings › Scientific › peer-review

TY - GEN

T1 - Scalable methods of discrete plant model generation for closed-loop model checking

AU - Buzhinskii, Igor

AU - Pakonen, Antti

AU - Vyatkin, Valeriy

N1 - Conference code: 43

PY - 2017/12/18

Y1 - 2017/12/18

N2 - To facilitate correctness and safety of mission-critical automation systems, formal methods should be applied in addition to simulation and testing. One of such formal methods is model checking, which is capable of verifying complex requirements for the system's model. If both the controller and the controlled plant are formally modeled, then the variant of this technique called closed-loop model checking can be applied. Recently, a technique of automatic plant model generation has been proposed which is applicable in this scenario. This paper continues the work in this direction by presenting two plant model construction approaches which are much more scalable with respect to the previous one, and puts this work into a more practical context. The approaches are evaluated on a case study from the nuclear automation domain.

AB - To facilitate correctness and safety of mission-critical automation systems, formal methods should be applied in addition to simulation and testing. One of such formal methods is model checking, which is capable of verifying complex requirements for the system's model. If both the controller and the controlled plant are formally modeled, then the variant of this technique called closed-loop model checking can be applied. Recently, a technique of automatic plant model generation has been proposed which is applicable in this scenario. This paper continues the work in this direction by presenting two plant model construction approaches which are much more scalable with respect to the previous one, and puts this work into a more practical context. The approaches are evaluated on a case study from the nuclear automation domain.

KW - model checking

KW - solid modeling

KW - automation

KW - computational modeling

KW - context modeling

KW - data models

KW - tools

U2 - 10.1109/IECON.2017.8216949

DO - 10.1109/IECON.2017.8216949

M3 - Conference article in proceedings

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

SP - 5483

EP - 5488

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 -

Scalable methods of discrete plant model generation for closed-loop model checking

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this