Plant Model Generator from Digital Twin for Purpose of Formal Verification

Simple item page
dc.contributorAalto-yliopistofi
dc.contributorAalto Universityen
dc.contributor.authorXavier, Midhunen_US
dc.contributor.authorHåkansson, Johannesen_US
dc.contributor.authorPatil, Sandeepen_US
dc.contributor.authorVyatkin, Valeriyen_US
dc.contributor.departmentDepartment of Electrical Engineering and Automationen
dc.contributor.groupauthorInformation Technologies in Industrial Automationen
dc.contributor.organizationLuleå University of Technologyen_US
dc.date.accessioned2022-02-02T07:50:43Z
dc.date.available2022-02-02T07:50:43Z
dc.date.issued2021-11-30en_US
dc.descriptionFunding 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.
dc.description.abstractThis 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.en
dc.description.versionPeer revieweden
dc.format.extent4
dc.format.mimetypeapplication/pdfen_US
dc.identifier.citationXavier, 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.9613704en
dc.identifier.doi10.1109/ETFA45728.2021.9613704en_US
dc.identifier.isbn978-1-7281-2989-1
dc.identifier.otherPURE UUID: 511955d9-cdd4-43b6-a920-2caad90ef58fen_US
dc.identifier.otherPURE ITEMURL: https://research.aalto.fi/en/publications/511955d9-cdd4-43b6-a920-2caad90ef58fen_US
dc.identifier.otherPURE FILEURL: https://research.aalto.fi/files/78899393/ELEC_Xavier_etal_Plant_Model_Generator_from_DigitalTwin_IEEE_ETFA_2021.pdf
dc.identifier.urihttps://aaltodoc.aalto.fi/handle/123456789/112752
dc.identifier.urnURN:NBN:fi:aalto-202202021649
dc.language.isoenen
dc.relation.fundinginfoACKNOWLEDGMENT This work was sponsored, in part, by the H2020 project 1-SWARM co-funded by the European Commission (grant agreement: 871743).
dc.relation.ispartofIEEE International Conference on Emerging Technologies and Factory Automationen
dc.relation.ispartofseriesProceedings - 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021en
dc.rightsopenAccessen
dc.subject.keywordFormal verificationen_US
dc.subject.keywordModel synthesis from tracesen_US
dc.subject.keywordPlant Modellingen_US
dc.subject.keywordState machine generationen_US
dc.titlePlant Model Generator from Digital Twin for Purpose of Formal Verificationen
dc.typeA4 Artikkeli konferenssijulkaisussafi
dc.type.versionacceptedVersion

Files

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
ELEC_Xavier_etal_Plant_Model_Generator_from_DigitalTwin_IEEE_ETFA_2021.pdf
Size:
751.93 KB
Format:
Adobe Portable Document Format
Download

Collections

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