Abstract
Closed-loop model checking, a formal verification technique for industrial automation systems, increases the richness of specifications to be checked and often helps to reduce size of the state space to be verified compared with the open-loop case. To be applied, it needs two components - the controller and the plant models - to be coupled. While there are approaches for obtaining controller models from implementation, specification or behavior examples, little has been done regarding automation of plant model construction. 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 and temporal properties.
Original language | English |
---|---|
Title of host publication | Proceedings of the 14th IEEE International Conference on Industrial Informatics, INDIN 2016 |
Publisher | IEEE |
Pages | 736-739 |
Number of pages | 4 |
ISBN (Electronic) | 9781509028702 |
DOIs | |
Publication status | Published - 2016 |
MoE publication type | A4 Conference publication |
Event | IEEE International Conference on Industrial Informatics - Poitiers, France Duration: 19 Jul 2016 → 21 Jul 2016 Conference number: 14 https://ieee-indin2016.sciencesconf.org/ |
Publication series
Name | IEEE International Conference on Industrial Informatics |
---|---|
Publisher | IEEE |
ISSN (Print) | 1935-4576 |
ISSN (Electronic) | 2378-363X |
Conference
Conference | IEEE International Conference on Industrial Informatics |
---|---|
Abbreviated title | INDIN |
Country/Territory | France |
City | Poitiers |
Period | 19/07/2016 → 21/07/2016 |
Internet address |