Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties

Igor Buzhinsky*, Valeriy Vyatkin

*Tämän työn vastaava kirjoittaja

Tutkimustuotos: LehtiartikkeliArticleScientificvertaisarvioitu

29 Sitaatiot (Scopus)
154 Lataukset (Pure)

Abstrakti

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.

AlkuperäiskieliEnglanti
Artikkeli7857798
Sivut1521-1530
Sivumäärä10
JulkaisuIEEE Transactions on Industrial Informatics
Vuosikerta13
Numero4
DOI - pysyväislinkit
TilaJulkaistu - 1 elokuuta 2017
OKM-julkaisutyyppiA1 Julkaistu artikkeli, soviteltu

Sormenjälki

Sukella tutkimusaiheisiin 'Automatic Inference of Finite-State Plant Models From Traces and Temporal Properties'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä