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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021 |
| Publisher | IEEE |
| Number of pages | 4 |
| ISBN (Electronic) | 978-1-7281-2989-1 |
| DOIs | |
| Publication status | Published - 30 Nov 2021 |
| MoE publication type | A4 Conference publication |
| Event | IEEE International Conference on Emerging Technologies and Factory Automation - Västerås, Sweden Duration: 7 Sept 2021 → 10 Sept 2021 Conference number: 26 |
Conference
| Conference | IEEE International Conference on Emerging Technologies and Factory Automation |
|---|---|
| Abbreviated title | ETFA |
| Country/Territory | Sweden |
| City | Västerås |
| Period | 07/09/2021 → 10/09/2021 |
Keywords
- Formal verification
- Model synthesis from traces
- Plant Modelling
- State machine generation