This talk reflects upon 20 years long efforts of the speaker to apply model-checking based formal verification to the practice of industrial automation. These efforts were mainly happening in the academia with sporadic attempts to interact with industry.

From the very beginning, the closed-loop view on the systems under verification was taken.

Early works on the application of model-checking to verification of programs date back to early 90s, and the first works on closed-loop verification appeared a few years after, in the end of 90s.

The reason behind the closed-loop approach is two-fold. First and foremost, explicit modelling of the plant enables formulation of requirements in terms of the plant’s processes which makes more sense for the automation system owner.

Another reason is that the closed-loop pattern promises lower complexity of model-checking than that of open-loop systems.

Another feature of the modern automation systems is modularity, and this feature is becoming increasingly more obvious. This requires modularization and “aspectisation” of the formal models as well, leading to the concept of cyber-physical component as an artefact used in both engineering and verification. To increase industrial applicability of this concept, we tried to rely on industrial standards for defining the input to our verification tools.

The fundamental question in the closed-loop approach is how to develop models of the plant systematically and with less effort. In recent works, we explored ideas of using simulation models as a source for generating automatically discrete state models using evolutionary algorithms or other heuristics. We also tried to limit evolutions of the plant to those which the controller under verification could bring the plant to, trying to “infuse” non-determinism on a limited scale.

The talk will touch upon several techniques aiming at practical applicability of model-checking and its use by the practicing control engineers.