Plant Model Generator from Digital Twin for Purpose of Formal Verification

Loading...
Thumbnail Image

Access rights

openAccess
acceptedVersion

URL

Journal Title

Journal ISSN

Volume Title

A4 Artikkeli konferenssijulkaisussa

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