Plant Model Generator from Digital Twin for Purpose of Formal Verification

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

Keywords

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

DOI

10.1109/ETFA45728.2021.9613704

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

Permanent link to this item

https://urn.fi/URN:NBN:fi:aalto-202202021649

Collections

[article-cris] Sähkötekniikan korkeakoulu / ELEC

Show all metadata