Plant model inference for closed-loop verification of control systems: Initial explorations

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.