Um komplexe Geschäftsanwendungen automatisiert oder manuell testen zu können, werden technisch korrekte Testdaten benötigt. Wir gehen hier davon aus, dass die Geschäftsanwendungen modellbasiert sind und dass die Modelle aus Feldern unterschiedlicher Typen sowie aus komplexen Validierungsregeln bestehen, die in einer standardisierten Regelsprache formuliert sind (siehe Abbildung 1).
Abb. 1: Visualisierung eines (realen) fachlichen Modells: Validierungsegeln stellen Beziehungen zwischen Feldern her
Die Regeln definieren, welche Werte in den Daten zulässig sind, und stellen Beziehungen zwischen den Feldern her. Gültige Testdaten dürfen die Regeln nicht verletzen.
In der Regel erfordert das manuelle Erstellen und Pflegen solcher Testdaten den Einsatz großer Teams von Fachexperten und ist mit beträchtlichem Aufwand verbunden. Darum ist es wünschenswert, die Testdaten automatisiert und ohne zusätzliches Fachwissen einfach auf Basis der fachlichen Modelle generieren zu können. Dies ist allerdings keine einfache Aufgabe, da die Validierungsregeln den Prozess erheblich erschweren.
Eine mögliche Herangehensweise besteht darin, einen Brute-Force-Ansatz zu nutzen. Dabei werden zufällige Testdaten erzeugt, die anschließend auf ihre Gültigkeit überprüft werden. Gültige Testdaten werden behalten, ungültige werden verworfen.
Für diesen Ansatz spricht, dass die zufällige Erzeugung von Testdaten sehr einfach und performant möglich ist. Typischerweise ist die Validierung der Daten anhand der Validierungsregeln ebenfalls einfach. Allerdings sinkt die Wahrscheinlichkeit, einen gültigen Datensatz zu finden, exponentiell mit der Anzahl der Felder und Regeln. Beispielsweise benötigt ein Rechner bereits bei einem kleinen Formular mit 100 Feldern und 100 Regeln mehrere Tage, um mit einer Wahrscheinlichkeit von 50 Prozent einen einzigen gültigen Datensatz zu generieren. Bereits bei mittelgroßen Formularen würde die benötigte Rechenzeit sogar länger sein als das Alter des Universums seit dem Urknall.
Im Labyrinth der Möglichkeiten: Widersprüche und richtige Abzweigungen
Darum ist es bei der Generierung von Testdaten von entscheidender Bedeutung, die Validierungsregeln in den Modellen zu analysieren. Doch in vielen Fällen bestehen solche Regeln aus mehreren Teilbedingungen, die durch „Oder“ miteinander verknüpft sind. Das bedeutet, es gibt mehrere Möglichkeiten, sie nicht zu verletzen.
Wer automatisiert Testdaten erzeugen möchte, muss für jede Regel entscheiden, welche Möglichkeit er wählt. Jede dieser Entscheidungen gleicht einer Abzweigung in einem komplexen Labyrinth. Die Größe dieses Labyrinths wächst ebenfalls exponentiell mit der Anzahl der „Oder“-Verknüpfungen.
Bereits bei mittelgroßen Formularen sprengt die schiere Größe praktisch jede Rechenkapazität. Zudem führen typischerweise die meisten Abzweigungen zu Sackgassen. Aus diesem Grund gestaltet sich die Suche nach einem Weg durch dieses schier unendliche Labyrinth äußerst herausfordernd.
Auswege aus dem Labyrinth: der SMT-Solver
Zum Glück gibt es spezielle Algorithmen, die genau auf solche Problemstellungen spezialisiert sind und in der Informatik und Mathematik zum Bereich der sogenannten „satisfiability modulo theories“ (SMT, etwa: Erfüllbarkeits-Modulo-Theorien) gehören.
Für den Einsatz in der Praxis gibt es spezielle SMT-Solver, die die Algorithmen in Bibliotheken bereitstellen. Und es gibt die standardisierte Sprache SMT-LIB [SMTLIB], um mit den SMT-Solvern zu kommunizieren.
Um einen SMT-Solver für die automatische Testdatengenerierung einsetzen zu können, werden die technischen Regeln aus der plattformspezifischen Regelsprache in SMT-LIB übersetzt. Das Ergebnis ist ein Gleichungssystem, das vom SMT-Solver gelöst wird. Die ermittelte Lösung wird anschließend wieder in einen Datensatz für die entsprechende Plattform übersetzt (siehe Abbildung 2).
Abb. 2: Beispiel: Übersetzung technischer Regeln aus plattformspezifischer Regelsprache in SMT-LIB
Angenommen, in einem Modell gibt es die Felder DatumsFeld1 und DatumsFeld2. Es ist eine Anforderung, dass Datums-Feld2 immer ein späteres Datum als DatumsFeld1 enthält. Im Modell wird eine Validierungsregel definiert, um dies zu gewährleisten. Diese Regel beschreibt immer den Fall eines Fehlers. In diesem Fall tritt ein Fehler auf, wenn sowohl DatumsFeld1 als auch DatumsFeld2 angegeben sind und der Wert in DatumsFeld1 größer oder gleich dem Wert in DatumsFeld2 ist.
Die entsprechende Validierungsregel lautet:
[DatumsFeld1] >= [DatumsFeld2]
Da es in SMT-LIB keinen Typ „Datum“ gibt, wird DatumsFeld1 in vier Variablen übersetzt: Dabei gibt es die Boolesche Variable DatumsFeld1-B, die den Wert wahr annimmt, wenn das Feld angegeben ist. Weiter gibt es die drei Integer-Variablen DatumsFeld1-y, DatumsFeld1-m und DatumsFeld1-d für Jahr, Monat und Tag. Die Übersetzung von DatumsFeld2 erfolgt analog.
Die genannte Validierungsregel in SMT-LIB zeigt Listing 1.
Listing 1: Validierungsregel in SMT-LIB mit zwei Datumsfeldern
In SMT-LIB erfolgt die Verwendung von Operatoren durch eine vorangestellte Notation. Darüber hinaus werden in SMT-LIB Regeln positiv formuliert, weshalb der Regel ein „not“ vorangestellt werden muss.
Herausforderungen bei der Nutzung von SMT-Solvern
Dieses Verfahren erfordert jedoch eine Übersetzung der kompletten plattformspezifischen Regelsprache: Für jedes Feld und für jede Regel wird eine Entsprechung in SMT-LIB benötigt. Es kann erforderlich sein, dass Felder auf mehrere Variablen in SMT-LIB gemappt werden müssen (wie im obigen Beispiel), weil in SMT-LIB kein entsprechender Typ existiert. Außerdem sind die Sprachkonstrukte der Regelsprache oft nicht eins zu eins übersetzbar und erfordern komplexere Umschreibungen in SMT-LIB.
Die zweite große Herausforderung liegt in der Leistungsfähigkeit der SMT-Solver. Es besteht die Gefahr einer exponentiell zunehmenden Rechenzeit, was an der Komplexität des Problems liegt, wie zuvor erläutert. Die Performance wird durch Faktoren wie die Größe und Komplexität des Modells, die Art der Übersetzung der Regelsprache in SMT-LIB und die generelle Handhabung des SMT-Solver beeinflusst.
Obwohl die SMT-Solver immer weiter verbessert werden, kann die automatische Testdatenerzeugung bei großen Modellen mit komplexen Regelwerken Stunden in Anspruch nehmen. Schon der kleinste Fehltritt, wie beispielsweise eine ungünstige Übersetzung der Regeln nach SMT-LIB, kann zu enormen Laufzeitverzögerungen bei der Performance führen. Typischerweise werden Geschäftsanwendungen und ihre fachlichen Modelle immer umfangreicher und komplexer. Daher ist es wichtig, kontinuierlich in die Verbesserung der Performance zu investieren, um mit der steigenden Komplexität der Fachlichkeit in den Formularen Schritt zu halten.
Praxisbeispiel für den Einsatz: Mein ELSTER
Ein solches komplexes System ist die Online-Plattform für die elektronische Steuererklärung Mein ELSTER [BLFST], für die unter anderem zu Testzwecken der A12-Testdatengenerator entwickelt wurde. Er erzeugt nach dem hier beschriebenen Verfahren automatisiert gültige Testdaten für Mein ELSTER. Mein ELSTER enthält mehr als 600 Formulare mit über 10.000 Seiten, 300.000 Feldern und 160.000 Regeln. Formulare, Felder und Regeln ändern sich oft. Eine manuelle Erzeugung und Aktualisierung der Testdaten, die wir für automatisierte und manuelle Tests benötigen, ist praktisch unmöglich.
Die Arbeitsweise des Testdatengenerators in Kurzform: Die Testdatengenerierung erfolgt vollautomatisch auf Basis der fachlichen Modelle. Zusätzliches Fachwissen ist nicht erforderlich. Die Testdaten testen alle Formulare vollständig.
Die Komplexität der Testdatengenerierung im ELSTER-Projekt hängt stark vom Formular ab. Die größten Formulare enthalten über 2.000 Felder und 2.000 Regeln, die jedoch wiederholt werden können. Das aktuell größte Modell in SMT-LIB enthält 12.590 Variablen und 12.446 Regeln. Die Laufzeit einer Testdatengenerierung (ca. 50 Datensätze) liegt bei kleineren Modellen im Sekundenbereich, bei den größten im Bereich von mehreren Stunden.
Vielfältige Testdaten für unterschiedliche Anwendungsfälle
Die SMT-Solver geben einen beliebigen Datensatz zurück, der in der Regel so einfach wie möglich ist. Daher müssen sie durch zusätzliche Regeln gezwungen werden, „interessante“ Werte in die Modelle einzutragen. Eine solche Zusatzregel könnte zum Beispiel sein, dass ein Feld leer bleiben oder mit einem bestimmten Wert gefüllt werden soll. Wenn der SMT-Solver zurückmeldet, dass diese Regel zusammen mit den bisherigen Regeln lösbar („satisfiable“) ist, verbleibt die zusätzliche Regel im SMT-Solver. Führt die zusätzliche Regel zu einem Widerspruch („unsatisfiable“), wird sie wieder entfernt. So werden die Variablen des Modells Schritt für Schritt mit tatsächlichen Werten gefüllt.
Durch die Anwendung von verschiedenen Zusatzregeln lassen sich verschiedene Arten von Datensätzen für unterschiedliche Anwendungsfälle erzeugen, zum Beispiel Minimal- und Maximaltestfälle.
Weitere Nutzungsmöglichkeiten
Das Mapping eines fachlichen Modells auf SMT-LIB bietet noch weitere Einsatzmöglichkeiten. Ein Beispiel hierfür ist das Erkennen von Regelwidersprüchen. So geben die SMT-Solver die Information zurück, ob ein Modell überhaupt lösbar ist. Ist das nicht der Fall, können sie die Regeln zurückgeben, die miteinander im Widerspruch stehen. Diese Funktionalität kann auch unter Hinzunahme von Vorbedingungen genutzt werden.
Im oben genannten A12-Testdatengenerator wird als Vorbedingung angenommen, dass in jedes Feld ein Wert eingebbar sein muss. Wenn die Validierungsregeln verhindern, dass ein Feld in irgendeinem fehlerfreien Datensatz angegeben werden kann, liegt ein logischer Fehler in den Validierungsregeln vor.
Das Verfahren dient somit nicht nur der Erzeugung von Testdaten, sondern auch der Qualitätssicherung der Validierungsregeln und der Fehlerbehebung.
Weitere Informationen
[BLFST] ELektronische STeuerERklärung, Bayerisches Landesamt für Steuern – Dienststelle München,
www.elster.de/eportal/infoseite/elster_eine_erfolgsstory
[NEGZ] B. Rumpe et al, Nationalen E-Government Kompetenzzentrum e. V., 2021,
idst.tax/wp-content/uploads/2021/06/NEGZ-Kurzstudie-19-Digitalisierung-der-Gesetzgebung-2021.pdf
[SMTLIB] smtlib.cs.uiowa.edu/
