Plant Model Generator from Digital Twin for Purpose of Formal Verification
2021 (English)In: 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), IEEE, 2021, p. 1-4Conference paper, Published paper (Refereed)
Abstract [en]
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.
Place, publisher, year, edition, pages
IEEE, 2021. p. 1-4
Keywords [en]
Visualization, Codes, Digital twin, Conferences, Tools, Software, Generators, Model synthesis from traces, Formal verification, Plant Modelling, State machine generation
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-88445DOI: 10.1109/ETFA45728.2021.9613704ISI: 000766992600252Scopus ID: 2-s2.0-85122951757OAI: oai:DiVA.org:ltu-88445DiVA, id: diva2:1620681
Conference
26th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2021), Västerås, Sweden, September 7-10, 2021
Note
ISBN för värdpublikation: 978-1-7281-2989-1, 978-1-7281-2990-7
2021-12-162021-12-162022-11-21Bibliographically approved