Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Automatic Inference of Finite-State Plant Models from Traces and Temporal Properties
Department of Electrical Engineering and Automation, Aalto University.
Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.ORCID-id: 0000-0002-9315-9920
2017 (Engelska)Ingår i: IEEE Transactions on Industrial Informatics, ISSN 1551-3203, E-ISSN 1941-0050, Vol. 13, nr 4, s. 1521-1530, artikel-id 7857798Artikel i tidskrift (Refereegranskat) Published
Abstract [en]

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.

Ort, förlag, år, upplaga, sidor
Institute of Electrical and Electronics Engineers (IEEE), 2017. Vol. 13, nr 4, s. 1521-1530, artikel-id 7857798
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Kommunikations- och beräkningssystem
Identifikatorer
URN: urn:nbn:se:ltu:diva-64252DOI: 10.1109/TII.2017.2670146ISI: 000406933400005Scopus ID: 2-s2.0-85029439382OAI: oai:DiVA.org:ltu-64252DiVA, id: diva2:1112179
Anmärkning

Validerad;2017;Nivå 2;2017-08-09 (rokbeg)

Tillgänglig från: 2017-06-20 Skapad: 2017-06-20 Senast uppdaterad: 2018-07-10Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Vyatkin, Valeriy

Sök vidare i DiVA

Av författaren/redaktören
Vyatkin, Valeriy
Av organisationen
Datavetenskap
I samma tidskrift
IEEE Transactions on Industrial Informatics
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 87 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf