Efficient Constraint Validation using Formal Methods in Combinatorial Testing

Abstract

Kombinatorisches Testen (CT) ist eine Black-Box-Testmethodik, die eingesetzt werden kann, um komplexe Systeme effektiv zu testen und dabei mathematische Abdeckungsgarantien zu liefern. Allerdings ist die Konstruktion kombinatorischer Testmengen eine anspruchsvolle Aufgabe, insbesondere bei Vorhandensein von Einschränkungen, die es Anwendern ermöglichen, unzulässige Kombinationen von Parametern und Werten zu spezifizieren. Ein wesentlicher Bestandteil der Generierung kombinatorischer Tests mit Einschränkungen ist die Validierung von Tests und Wertzuweisungen, im Folgenden als Einschränkungsvalidierung bezeichnet. In der Literatur wurden zahlreiche Ansätze zur Einschränkungsvalidierung vorgeschlagen, darunter Methoden auf Basis verbotener Tupel, SAT-Solver, CSP- und SMT-Solver sowie binärer Entscheidungsdiagramme. Während Übersichtsarbeiten zur Behandlung von Einschränkungen im kombinatorischen Testen existieren, fehlt bislang ein umfassender Vergleich der Leistungsfähigkeit dieser Validierungsmethoden. Diese Arbeit evaluiert die Leistungsfähigkeit mehrerer Methoden zur Einschränkungsvalidierung, einschließlich unterschiedlicher Kodierungen und Optimierungen, und untersucht, wie Faktoren wie die Anzahl der Parameter, Alphabetgrößen und die Komplexität der Einschränkungen diese beeinflussen. Zu diesem Zweck wurden alle im Rahmen einer umfangreichen Literaturrecherche identifizierten Validierungsmethoden, Kodierungen und Optimierungen in einem einheitlichen Framework implementiert. Darüber hinaus wurde ein Benchmark-Generator entwickelt, um synthetische Eingabeparametermodelle (IPMs) zu erzeugen, die in Kategorien mit unterschiedlichen Eigenschaften gruppiert werden können. Eine umfassende experimentelle Evaluierung wurde sowohl auf einem Benchmark-Satz bestehend aus sechzig solcher Kategorien mit jeweils zehn IPMs als auch auf dem Benchmark-Satz des IWCT-2023-CT-Wettbewerbs durchgeführt, der reale Instanzen beinhaltet. Durch die Fokussierung auf generische Aufgaben der Einschränkungsvalidierung sind die Ergebnisse auf eine Vielzahl von Algorithmen und Anwendungsbereichen übertragbar. Die Ergebnisse zeigen, dass es keinen universell besten Ansatz für alle Aufgaben gibt. Während die leistungsfähigste Methode in erster Linie von der Komplexität der Einschränkungen abhängt, spielen auch Faktoren wie die Anzahl der Parameter, deren Alphabetgrößen sowie die konkrete Validierungsaufgabe eine bedeutende Rolle. Die Erkenntnisse dieser Arbeit können praktische Hinweise zur Auswahl geeigneter Methoden der Einschränkungsvalidierung liefern und die Entwicklung effizienterer Werkzeuge für das kombinatorische Testen unterstützen.

Combinatorial testing (CT) is a black-box testing methodology that can be used to effectively test complex systems while providing mathematical coverage guarantees. However, constructing combinatorial test sets is a challenging task, particularly in the presence of constraints, which allow practitioners to specify forbidden combinations of parameters and values. An integral part of constrained combinatorial test generation is the validation of tests and value assignments, here referred to as constraint validation. Numerous constraint validation approaches have been proposed in the literature, including methods based on forbidden tuples, SAT solvers, CSP and SMT solvers, as well as binary decision diagrams. While surveys of constraint handling in combinatorial testing exist, a comprehensive comparison of the performance of these validation methods is still missing. This thesis evaluates the performance of multiple constraint validation methods, including different encodings and optimizations, and investigates how factors such as the number of parameters, alphabet sizes, and constraint complexity influence their performance. To this end, all validation methods, encodings, and optimizations identified in an extensive literature search were implemented in a unified framework. Furthermore, a benchmark generator was developed to create synthetic input parameter models (IPMs) that can be grouped into categories with distinct characteristics. A comprehensive experimental evaluation was conducted on a benchmark set consisting of sixty such categories, each comprising ten IPMs, as well as on the benchmark set of the IWCT 2023 CT competition, which includes real-world instances. By focusing on generic constraint validation tasks, the results are applicable to a wide range of algorithms and application areas. The results demonstrate that no universally best approach exists for all tasks. While the best-performing method depends primarily on the complexity of the constraints, factors such as the number of parameters, their alphabet sizes, as well as the specific validation task also play a significant role. The findings of this work can provide practical guidance for selecting suitable constraint validation techniques and support the development of more efficient combinatorial testing tools.