Plant Model Generator from Digital Twin for Purpose of Formal Verification
Loading...
Access rights
openAccess
acceptedVersion
URL
Journal Title
Journal ISSN
Volume Title
A4 Artikkeli konferenssijulkaisussa
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
Date
2021-11-30
Major/Subject
Mcode
Degree programme
Language
en
Pages
4
Series
Proceedings - 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021
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.Description
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: © 2021 IEEE.
Keywords
Formal verification, Model synthesis from traces, Plant Modelling, State machine generation
Other note
Citation
Xavier, M, Håkansson, J, Patil, S & Vyatkin, V 2021, Plant Model Generator from Digital Twin for Purpose of Formal Verification . in 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, Sweden, 07/09/2021 . https://doi.org/10.1109/ETFA45728.2021.9613704