Plant Model Generator from Digital Twin for Purpose of Formal Verification

Midhun Xavier; Johannes Håkansson; Sandeep Patil; Valeriy Vyatkin

doi:10.1109/ETFA45728.2021.9613704

Plant Model Generator from Digital Twin for Purpose of Formal Verification

Midhun Xavier, Johannes Håkansson, Sandeep Patil, Valeriy Vyatkin

Luleå University of Technology

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

6 Sitaatiot (Scopus)

54 Lataukset (Pure)

Abstrakti

This paper reports on a method of automatic generation of a formal model of plant from the behaviour traces recorded from its digital twin. The traces are observed from simulation in the loop of the digital twin in Visual Components connected with distributed automation software, developed in NxtSTUDIO according to IEC 61499. The generated modular formal model of the closed-loop system is transformed to the model of uncontrolled plant behaviour extended with nondeterminism. The model is then combined in closed-loop with the formal model of controller, generated from its source code using the fb2smv tool. The verification and simulation is done by the symbolic model checker NuSMV tool, which verifies various CTL/LTL specifications of the system.

Alkuperäiskieli	Englanti
Otsikko	Proceedings - 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021
Kustantaja	IEEE
Sivumäärä	4
ISBN (elektroninen)	978-1-7281-2989-1
DOI - pysyväislinkit	https://doi.org/10.1109/ETFA45728.2021.9613704
Tila	Julkaistu - 30 marrask. 2021
OKM-julkaisutyyppi	A4 Artikkeli konferenssijulkaisussa
Tapahtuma	IEEE International Conference on Emerging Technologies and Factory Automation - Västerås, Ruotsi Kesto: 7 syysk. 2021 → 10 syysk. 2021 Konferenssinumero: 26

Conference

Conference	IEEE International Conference on Emerging Technologies and Factory Automation
Lyhennettä	ETFA
Maa/Alue	Ruotsi
Kaupunki	Västerås
Ajanjakso	07/09/2021 → 10/09/2021

Pääsy asiakirjaan

10.1109/ETFA45728.2021.9613704

ELEC_Xavier_etal_Plant_Model_Generator_from_DigitalTwin_IEEE_ETFA_2021Accepted author manuscript, 516 KB

Muut tiedostot ja linkit

Linkki julkaisuun Scopuksessa

Siteeraa tätä

@inproceedings{511955d9cdd443b6a9202caad90ef58f,

title = "Plant Model Generator from Digital Twin for Purpose of Formal Verification",

abstract = "This paper reports on a method of automatic generation of a formal model of plant from the behaviour traces recorded from its digital twin. The traces are observed from simulation in the loop of the digital twin in Visual Components connected with distributed automation software, developed in NxtSTUDIO according to IEC 61499. The generated modular formal model of the closed-loop system is transformed to the model of uncontrolled plant behaviour extended with nondeterminism. The model is then combined in closed-loop with the formal model of controller, generated from its source code using the fb2smv tool. The verification and simulation is done by the symbolic model checker NuSMV tool, which verifies various CTL/LTL specifications of the system.",

keywords = "Formal verification, Model synthesis from traces, Plant Modelling, State machine generation",

author = "Midhun Xavier and Johannes H{\aa}kansson and Sandeep Patil and Valeriy Vyatkin",

note = "Funding Information: ACKNOWLEDGMENT This work was sponsored, in part, by the H2020 project 1-SWARM co-funded by the European Commission (grant agreement: 871743). Publisher Copyright: {\textcopyright} 2021 IEEE.; IEEE International Conference on Emerging Technologies and Factory Automation, ETFA ; Conference date: 07-09-2021 Through 10-09-2021",

year = "2021",

month = nov,

day = "30",

doi = "10.1109/ETFA45728.2021.9613704",

language = "English",

booktitle = "Proceedings - 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021",

publisher = "IEEE",

address = "United States",

}

Xavier, M, Håkansson, J, Patil, S & Vyatkin, V 2021, Plant Model Generator from Digital Twin for Purpose of Formal Verification. julkaisussa Proceedings - 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021. IEEE, IEEE International Conference on Emerging Technologies and Factory Automation, Västerås, Ruotsi, 07/09/2021. https://doi.org/10.1109/ETFA45728.2021.9613704

Plant Model Generator from Digital Twin for Purpose of Formal Verification. / Xavier, Midhun; Håkansson, Johannes; Patil, Sandeep et al.
Proceedings - 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021. IEEE, 2021.

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

TY - GEN

T1 - Plant Model Generator from Digital Twin for Purpose of Formal Verification

AU - Xavier, Midhun

AU - Håkansson, Johannes

AU - Patil, Sandeep

AU - Vyatkin, Valeriy

N1 - Conference code: 26

PY - 2021/11/30

Y1 - 2021/11/30

N2 - This paper reports on a method of automatic generation of a formal model of plant from the behaviour traces recorded from its digital twin. The traces are observed from simulation in the loop of the digital twin in Visual Components connected with distributed automation software, developed in NxtSTUDIO according to IEC 61499. The generated modular formal model of the closed-loop system is transformed to the model of uncontrolled plant behaviour extended with nondeterminism. The model is then combined in closed-loop with the formal model of controller, generated from its source code using the fb2smv tool. The verification and simulation is done by the symbolic model checker NuSMV tool, which verifies various CTL/LTL specifications of the system.

AB - This paper reports on a method of automatic generation of a formal model of plant from the behaviour traces recorded from its digital twin. The traces are observed from simulation in the loop of the digital twin in Visual Components connected with distributed automation software, developed in NxtSTUDIO according to IEC 61499. The generated modular formal model of the closed-loop system is transformed to the model of uncontrolled plant behaviour extended with nondeterminism. The model is then combined in closed-loop with the formal model of controller, generated from its source code using the fb2smv tool. The verification and simulation is done by the symbolic model checker NuSMV tool, which verifies various CTL/LTL specifications of the system.

KW - Formal verification

KW - Model synthesis from traces

KW - Plant Modelling

KW - State machine generation

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

U2 - 10.1109/ETFA45728.2021.9613704

DO - 10.1109/ETFA45728.2021.9613704

M3 - Conference article in proceedings

AN - SCOPUS:85122951757

BT - Proceedings - 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021

PB - IEEE

T2 - IEEE International Conference on Emerging Technologies and Factory Automation

Y2 - 7 September 2021 through 10 September 2021

ER -

Plant Model Generator from Digital Twin for Purpose of Formal Verification

Abstrakti

Conference

Pääsy asiakirjaan

Muut tiedostot ja linkit

Sormenjälki

Siteeraa tätä