Combining closed-loop test generation and execution by means of model checking

TL;DR

This paper introduces a hybrid framework combining model checking and testing to verify industrial automation systems efficiently, balancing reliability and computational complexity, especially for closed-loop models.

Contribution

It proposes a novel approach that integrates model checking with test generation and execution for closed-loop systems, enhancing verification efficiency.

Findings

Framework achieves a trade-off between reliability and computational effort.

Supports closed-loop models including both controller and plant.

Enables targeted verification through test suite coverage.

Abstract

Model checking is an established technique to formally verify automation systems which are required to be trusted. However, for sufficiently complex systems model checking becomes computationally infeasible. On the other hand, testing, which offers less reliability, often does not present a serious computational challenge. Searching for synergies between these two approaches, this paper proposes a framework to ensure reliability of industrial automation systems by means of hybrid use of model checking and testing. This framework represents a way to achieve a trade-off between verification reliability and computational complexity which has not yet been explored in other approaches. Instead of undergoing usual model checking, system requirements are checked only on particular system behaviors which represent a test suite achieving coverage for both the system and the requirements. Then, all stages of the framework support the case of a closed-loop model, where not only the controller, but also the plant is modeled.