Automated Production Systems (aPS) in regulated industries such as pharmaceuticals, MedTech, or food and beverages must comply with the stringent validation and documentation requirements of Good Manufacturing Practice (GMP) regulations within the European Union (EU). These obligations create significant burdens for aPS manufacturers, particularly when changes require revalidation through manual integration and system testing. But these prerequisites also enable opportunities for lower-effort software verification, leveraging GMP documentation and boundaries of the automation domain to prove, e.g., that an implemented software change realizes the change specification without side effects. This paper proposes a methodical workflow for deriving software slices suitable for formal verification, while being aligned with automation engineering practices and GMP requirements. It defines assumptions for slice utility based on system modularity, interface expressiveness, and domain boundaries. The approach is validated through a real-world GMP-regulated change from a German MedTech aPS manufacturer, following GAMP 5 guidelines, demonstrating the utility for GMP-regulated aPS engineering and automatic verification of a sliced program segment.

Abstract The KeY tool is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable. KeY combines auto-active and fine-grained proof interaction, which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date. The article provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods.

Hash maps are a common and important data structure in efficient algorithm implementations. Despite their wide-spread use, real-world implementations are not regularly verified. In this article, we present the first case study of the IdentityHashMap class in the Java JDK. We specified its behavior using the Java Modeling Language (JML) and proved correctness for the main insertion and lookup methods with KeY, a semi-interactive theorem prover for JML-annotated Java programs. Furthermore, we report how unit testing and bounded model checking can be leveraged to find a suitable specification more quickly. We also investigated where the bottlenecks in the verification of hash maps lie for KeY by comparing required automatic proof effort for different hash map implementations and draw conclusions for the choice of hash map implementations regarding their verifiability.

Type systems and modern type checkers can be used very successfully to obtain formal correctness guarantees with little specification overhead. However, type systems in practical scenarios have to trade precision for decidability and scalability. Tools for deductive verification, on the other hand, can prove general properties in more cases than a typical type checker can, but they do not scale well. We present a method to complement the scalability of expressive type systems with the precision of deductive program verification approaches. This is achieved by translating the type uses whose correctness the type checker cannot prove into assertions in a specification language, which can be dealt with by a deductive verification tool. Type uses whose correctness the type checker can prove are instead turned into assumptions to aid the verification tool in finding a proof.Our novel approach is introduced both conceptually for a simple imperative language, and practically by a concrete implementation for the Java programming language. The usefulness and power of our approach has been evaluated by discharging known false positives from a real-world program and by a small case study.

Modern large scale technical systems often face iterative changes on their behaviours with the requirement of validated quality which is not easy to achieve completely with traditional testing. Regression verification is a powerful tool for the formal correctness analysis of software-driven systems. By proving that a new revision of the software behaves similarly as the original version of the software, some of the trust that the old software and system had earned during the validation processes or operation histories can be inherited to the new revision. This trust inheritance by the formal analysis relies on a number of implicit assumptions which are not self-evident but easy to miss, and may lead to a false sense of safety induced by a misunderstood regression verification processes. This paper aims at pointing out hidden, implicit assumptions of regression verification in the context of cyber-physical systems by making them explicit using practical examples. The explicit trust inheritance analysis would clarify for the engineers to understand the extent of the trust that regression verification provides and consequently facilitate them to utilize this formal technique for the system validation.

High requirements regarding quality are set for automated production systems (aPS) as malfunctions can harm humans or cause severe financial loss. These malfunctions can be caused by faults in the control software of the aPS or its inability to correctly identify and handle unintended situations and errors in the technical process or hardware behavior. To achieve more dependable control software, software testing and formal verification can be used to find faults in the software, but require to make assumptions about possible situations (inputs) occurring in the aPS during runtime and often only allow the validation of specific cases. Monitoring individual functions within the control software during runtime can help to identify unspecified situations and raise warnings of the uncertainty about the suitability of a reaction. Yet, the design of reliable monitoring functions requires extensive experience and resources. For this reason, we propose a method for generating monitoring functions from available testing and verification specifications initially used for validating a control software function. Through this, it is possible to continuously assess the behavior of individual software functions and to identify and warn about a) violations of the test specification during runtime and b) unintended situations in which correct software behavior was never tested. Thus, the approach can help to assess and improve both the control software and specification quality through observation and behavior assessment far beyond the testing phase by efficiently reusing existing test specifications for runtime monitoring.

With recent trends in manufacturing automation, such as Industry 4.0, control software in automated production systems becomes more and more complex and volatile, complicating and increasing importance of quality assurance. Test tables are a widely used and generally accepted means to intuitively specify test cases for automation software. However, each table only specifies a single software trace, whereas the actual software behavior may cover multiple similar traces not covered by the table. Within this work, we present a generalization concept for test tables allowing for bounded and unbounded repetition of steps, “don't-care” values, as well as calculations with earlier observed values. We provide a verification mechanism for checking conformance of an IEC 61131-3 PLC software with a generalized test table, making use of a state-of-the-art model checker. Our notation is inspired by widely-used paradigms found in spreadsheet applications. By an empirical study with mechanical engineering students, we show that the notation matches user expectations. A real-world example extracted from an industrial automation plant illustrates our approach.

Automated production systems are usually driven by Programmable Logic Controllers (PLCs). These systems are long-living and have high requirements for software quality to avoid downtimes, damaged product and harm to personnel. While commissioning multiple systems of similar type, pragmatic adjustments of the software are often necessary, which results in two or more similar variants of initially identical software. For further evolution of the software, an equivalence analysis of the software's behavior is beneficial to merge divergent development branches into a single program version. This paper presents a novel method for regression verification of PLC code, which allows one to prove that two variants of a plant's software behave identically in specified situations, despite being implemented differently. For this, a regression verification method for PLC code was designed, implemented and evaluated. The notion of program equivalence for reactive PLC code is clarified and defined. Core elements of the method are the translation of PLC code into the SMV input language for model checkers, the adaptation of the coupling invariants concept to reactive systems, and the implementation of a toolchain using a model checker. The approach was successfully evaluated using the Pick-and-Place Unit benchmark case study.