Plant model inference for closed-loop verification of control systems: Initial explorations

Igor Buzhinskii; Valeriy Vyatkin

doi:10.1109/INDIN.2016.7819256

Plant model inference for closed-loop verification of control systems: Initial explorations

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

Abstract

Closed-loop model checking, a formal verification technique for industrial automation systems, increases the richness of specifications to be checked and often helps to reduce size of the state space to be verified compared with the open-loop case. To be applied, it needs two components - the controller and the plant models - to be coupled. While there are approaches for obtaining controller models from implementation, specification or behavior examples, little has been done regarding automation of plant model construction. This paper aims to solve the problem of automatic plant model construction from existing specification, which is represented in the form of plant behavior examples and temporal properties.

Original language	English
Title of host publication	Proceedings of the 14th IEEE International Conference on Industrial Informatics, INDIN 2016
Publisher	IEEE
Pages	736-739
Number of pages	4
ISBN (Electronic)	9781509028702
DOIs	https://doi.org/10.1109/INDIN.2016.7819256
Publication status	Published - 2016
MoE publication type	A4 Article in a conference publication
Event	IEEE International Conference on Industrial Informatics - Poitiers, France Duration: 19 Jul 2016 → 21 Jul 2016 Conference number: 14 https://ieee-indin2016.sciencesconf.org/

Publication series

Name	IEEE International Conference on Industrial Informatics
Publisher	IEEE
ISSN (Print)	1935-4576
ISSN (Electronic)	2378-363X

Conference

Conference	IEEE International Conference on Industrial Informatics
Abbreviated title	INDIN
Country	France
City	Poitiers
Period	19/07/2016 → 21/07/2016
Internet address	https://ieee-indin2016.sciencesconf.org/

Access to Document

10.1109/INDIN.2016.7819256

Link to publication in Scopus

Fingerprint Dive into the research topics of 'Plant model inference for closed-loop verification of control systems: Initial explorations'. Together they form a unique fingerprint.

Cite this

@inproceedings{8be613990d684748b4a7f17564421ddb,

title = "Plant model inference for closed-loop verification of control systems: Initial explorations",

abstract = "Closed-loop model checking, a formal verification technique for industrial automation systems, increases the richness of specifications to be checked and often helps to reduce size of the state space to be verified compared with the open-loop case. To be applied, it needs two components - the controller and the plant models - to be coupled. While there are approaches for obtaining controller models from implementation, specification or behavior examples, little has been done regarding automation of plant model construction. This paper aims to solve the problem of automatic plant model construction from existing specification, which is represented in the form of plant behavior examples and temporal properties.",

author = "Igor Buzhinskii and Valeriy Vyatkin",

year = "2016",

doi = "10.1109/INDIN.2016.7819256",

language = "English",

series = "IEEE International Conference on Industrial Informatics",

publisher = "IEEE",

pages = "736--739",

booktitle = "Proceedings of the 14th IEEE International Conference on Industrial Informatics, INDIN 2016",

address = "United States",

note = "IEEE International Conference on Industrial Informatics, INDIN ; Conference date: 19-07-2016 Through 21-07-2016",

url = "https://ieee-indin2016.sciencesconf.org/",

}

Buzhinskii, I & Vyatkin, V 2016, Plant model inference for closed-loop verification of control systems: Initial explorations. in Proceedings of the 14th IEEE International Conference on Industrial Informatics, INDIN 2016., 7819256, IEEE International Conference on Industrial Informatics, IEEE, pp. 736-739, IEEE International Conference on Industrial Informatics, Poitiers, France, 19/07/2016. https://doi.org/10.1109/INDIN.2016.7819256

Plant model inference for closed-loop verification of control systems : Initial explorations. / Buzhinskii, Igor; Vyatkin, Valeriy.

Proceedings of the 14th IEEE International Conference on Industrial Informatics, INDIN 2016. IEEE, 2016. p. 736-739 7819256 (IEEE International Conference on Industrial Informatics).

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

TY - GEN

T1 - Plant model inference for closed-loop verification of control systems

T2 - IEEE International Conference on Industrial Informatics

AU - Buzhinskii, Igor

AU - Vyatkin, Valeriy

N1 - Conference code: 14

PY - 2016

Y1 - 2016

N2 - Closed-loop model checking, a formal verification technique for industrial automation systems, increases the richness of specifications to be checked and often helps to reduce size of the state space to be verified compared with the open-loop case. To be applied, it needs two components - the controller and the plant models - to be coupled. While there are approaches for obtaining controller models from implementation, specification or behavior examples, little has been done regarding automation of plant model construction. This paper aims to solve the problem of automatic plant model construction from existing specification, which is represented in the form of plant behavior examples and temporal properties.

AB - Closed-loop model checking, a formal verification technique for industrial automation systems, increases the richness of specifications to be checked and often helps to reduce size of the state space to be verified compared with the open-loop case. To be applied, it needs two components - the controller and the plant models - to be coupled. While there are approaches for obtaining controller models from implementation, specification or behavior examples, little has been done regarding automation of plant model construction. This paper aims to solve the problem of automatic plant model construction from existing specification, which is represented in the form of plant behavior examples and temporal properties.

UR - http://www.scopus.com/inward/record.url?scp=85012877880&partnerID=8YFLogxK

U2 - 10.1109/INDIN.2016.7819256

DO - 10.1109/INDIN.2016.7819256

M3 - Conference contribution

T3 - IEEE International Conference on Industrial Informatics

SP - 736

EP - 739

BT - Proceedings of the 14th IEEE International Conference on Industrial Informatics, INDIN 2016

PB - IEEE

Y2 - 19 July 2016 through 21 July 2016

ER -