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.

Several tools and approaches for proving non-interference properties for Java and other languages exist. Some of them have a high degree of automation or are even fully automatic, but over approximate the actual information flow, and hence, may produce false positives. Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence, analysis is time-consuming. In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches: We want to use fully automatic analysis as much as possible and only at places in a program where, due to over approximation, the automatic approaches fail, we resort to more precise, but interactive analysis, where the latter involves the verification only of specific functional properties in certain parts of the program, rather than checking more intricate non-interference properties for the whole program. To illustrate the hybrid approach, in a case study we use this approach - along with the fully automatic tool Joana for checking non-interference properties for Java programs and the theorem prover KeY for the verification of Java programs - as well as the CVJ framework proposed by Kuesters, Truderung, and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an e-voting system. The CVJ framework allows one to establish cryptographic indistinguishability properties for Java programs by checking (standard) non-interference properties for such programs.