Applicability of generalized test tables: a case study using the manufacturing system demonstrator xPPU

Steigende Kunden- und Marktanfordungen in der Fertigungsautomatisierung erfordern komplexere Steuerungssoftware und kürzere Entwicklungszyklen. Um zukünftig Korrektheit und Zuverlässigkeit sicherstellen zu können, ist eine Anpassung an der Qualitätssicherung erforderlich. Formale Methoden können hierfür nachprüfbare Garantien bieten, aber obwohl Automatisierungstechnik in unternehmenskritischen Bereichen eingesetzt wird, werden formale Methoden dort selten verwendet. Einer der Gründe ist der Mangel an geeigneten Spezifikationssprachen für die Automatisierungsdomäne, die sowohl nachvollziehbar als auch ausreichend aussagekräftig sind. ... mehrGeneralized Test Tables (GTTs) sind eine formale tabellen-basierte Spezifikationssprache für reaktive Systeme für den Entwicklungsingenieur. GTTs erhöhen die Aussagemächtigkeit und Testabdeckung konkreter Testtabellen unter Beibehaltung ihrer Verständlichkeit. In diesem Beitrag analysieren wir die Anwendbarkeit und Verständlichkeit von GTTs. Dazu spezifizieren wir Teile des Anlagenverhaltens diverser Szenarien aus dem Community Demonstrator Pick&Place-Unit (PPU).

With recent trends in manufacturing automation, control software in automated production systems becomes more complex and has more variability to keep pace with customer and market requirements. Quality assurance also becomes more and more important to ensure that the systems live up to expectations. However, correctness of automation software is rarely verified using formal techniques in spite of their high coverage. One of the main reasons is the lack of specification languages suitable for this application area that are both comprehensible and sufficiently expressive. ... mehrGeneralized test tables (GTTs), which are a specification language for reactive systems, were presented recently as an accessible representation for application engineers. This formalism achieves both the comprehensibility of concrete test tables and the coverage of formal methods. In our approach, the specification provided by GTTs is used for formal verification, especially model checking. In this paper, we present four new features for GTTs: the progression flag, strong repetition, row grouping, and specification on internal variables. We demonstrate the applicability and evaluate the comprehensibility of GTT-based specification and verification using a range of diverse scenarios from the community demonstrator, the extended Pick & Place Unit.