/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 73

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 73
" /> /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 78

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 78
" /> /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 96

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 96
"/> KIT - Application-oriented Formal Verification - <br /> <b>Warning</b>: Undefined array key "title" in <b>/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php</b> on line <b>99</b><br /> <br /> <b>Warning</b>: Attempt to read property "value" on null in <b>/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php</b> on line <b>99</b><br />
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive Systems Alexander Weigl, Franziska Wiebe, Mattias Ulbrich, Sebastian Ulewicz, Suhyun Cha, Michael Kirsten, Bernhard Beckert, and Birgit Vogel-Heuser 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.