Requirement verification in simulation-based automation testing

TL;DR

This paper proposes a simulation-based runtime verification method using Metric Temporal Logic to verify complex industrial automation systems, offering a scalable alternative to formal verification and testing.

Contribution

It introduces a novel application of Metric Temporal Logic for simulation-based verification in industrial automation, demonstrating practical scalability and effectiveness.

Findings

Successfully identified requirement violations in a real industrial process

Validated scalability of the approach in a complex production environment

Provides a practical verification method bridging formal methods and testing

Abstract

The emergence of the Industrial Internet results in an increasing number of complicated temporal interdependencies between automation systems and the processes to be controlled. There is a need for verification methods that scale better than formal verification methods and which are more exact than testing. Simulation-based runtime verification is proposed as such a method, and an application of Metric temporal logic is presented as a contribution. The practical scalability of the proposed approach is validated against a production process designed by an industrial partner, resulting in the discovery of requirement violations.