Formal Specification and Verification for Automated Production Systems

Complex industrial control software often drives safety- and mission-critical
systems, like automated production plants or control units embedded into devices in automotive systems. Such controllers have in common that they are reactive systems, i.e., that they periodically read sensor stimuli and cyclically execute the same program to produce actuator signals.

The correctness of software for automated production is rarely verified using
formal techniques. Although, due to the Industrial Revolution 4.0 (IR4.0), the
impact and importance of software have become an important role in industrial automation.

What is used instead in industrial practice today is testing and simulation,
where individual test cases are used to validate an automated production system.
Three reasons why formal methods are not popular are: (a) It is difficult to
adequately formulate the desired temporal properties. (b) There is a lack of
specification languages for reactive systems that are both sufficiently
expressive and comprehensible for practitioners. (c) Due to the lack of an
environment model the obtained results are imprecise. Nonetheless, formal
... mehr
methods for automated production systems are well studied academically---mainly on the verification of safety properties via model checking.

In this doctoral thesis we present the concept of (1) generalized test tables
(GTTs), a new specification language for functional properties, and their
extension (2) relational test tables (RTTs) for relational properties. The
concept includes the syntactical notion, designed for the intuition of
engineers, and the semantics, which are based on game theory. We use RTTs for a novel confidential property on reactive systems, the provably forgetting of information. Moreover, for regression verification, an important relational
property, we are able to achieve performance improvements by (3) creating
a decomposing rule which splits large proofs into small sub-task. We implemented the verification procedures and evaluated them against realistic case studies, e.g., the Pick-and-Place-Unit from the Technical University of Munich.

The presented contribution follows the idea of lowering the obstacle of
verifying the dependability of reactive systems in general, and automated
production systems in particular for the engineer either by introducing a new
specification language (GTTs), by exploiting existing programs for the
specification (RTTs, regression verification), or by improving the verification
performance.