Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties
No Thumbnail Available
Access rights
openAccess
URL
Journal Title
Journal ISSN
Volume Title
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
Authors
Date
2017-08-01
Major/Subject
Mcode
Degree programme
Language
en
Pages
10
1521-1530
1521-1530
Series
IEEE Transactions on Industrial Informatics, Volume 13, issue 4
Abstract
Closed-loop model checking, a formal verification technique for industrial automation systems, increases the richness of specifications to be checked and reduces the state space to be verified compared to the open-loop case. To be applied, it needs the controller and the plant formal models to be coupled. There are approaches for controller synthesis, but little has been done regarding plant model construction. While manual plant modeling is time consuming and error-prone, discretizing a simulation model of the plant leads to state excess. This paper aims to solve the problem of automatic plant model construction from existing specification, which is represented in the form of plant behavior examples, or traces, and temporal properties. The proposed method, which is based on the translation of the problem to the Boolean satisfiability problem, is evaluated and shown to be applicable on several case study plant model synthesis tasks and on randomly generated problem instances.Description
Keywords
Automatic model synthesis, closed-loop modeling, industrial automation software, model checking, SAT
Other note
Citation
Buzhinsky, I & Vyatkin, V 2017, ' Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties ', IEEE Transactions on Industrial Informatics, vol. 13, no. 4, 7857798, pp. 1521-1530 . https://doi.org/10.1109/TII.2017.2670146