CPOT-SM – Vollständiges eigenschaftsorientiertes Testen mit symbolischen Methoden

• Antragsteller: Professor Dr. Jan Peleska
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme ; Theoretische Informatik
• Förderung: Förderung von 2019 bis 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 407708394

Vollständige Testmethoden erlauben die Erzeugung von Testsuiten mit garantierten Fehleraufdeckungseigenschaften unter bestimmten Hypothesen über den Testling. Obwohl sie immer schon als interessantes Forschungsgebiet galten, ist ihre praktische Anwendbarkeit jedoch oft angezweifelt worden, da sie zu nicht mehr handhabbaren Testsuitegrößen führten, wenn man volle Fehlerabdeckung unter realistischen Hypothesen erzielen wollte. Diese Situation hat sich in den letzten Jahren geändert, da man zeigen konnte, dass sich Äquivalenzklassenverfahren auf Testlinge industrieller Größe anwenden lassen. In diesem Projekt ist geplant, diese neueren Ergebnisse im Kontext des Property-oriented Testing (POT, eigenschaftsorientiertes Testen) zu verwerten und auszuweiten. Im Gegensatz zum allgemeinen Modell-basierten Testen (MBT) konzentriert sich POT auf den umfassenden Test einzelner Anforderungen an den Testling. Daher erfordert POT keine vollständigen Modelle, welche das vollständige erwartete Verhalten des Testlings beschreiben. Stattdessen kann POT auf der Basis von (1) temporallogischen Spezifikationen, (2) partiellen Modellen oder (3) abstrahierten Modellen erfolgen. Infolgedessen sind die Kosten für eine Verifikation mittels POT üblicherweise niedriger als die Kosten für die Umsetzung des vollen MBT Ansatzes. Es gibt jedoch zur Zeit keine umfassende Theorie für die Vollständigkeit eingeschaftsprüfender Tests. Daher ist das Hauptziel dieses Projektes, neue POT-Ansätze zu entwickeln, nach denen sich Testsuiten mit garantierter Fehlerabdeckung erzeugen lassen. Dies wird durch einen kombinierten Ansatz erreicht, der sowohl Modelle, als auch temporallogische Spezifikationen verwendet. Um die Zustandsraumkomplexität der Modelle zu beherrschen, werden symbolische Methoden angewendet, mit Hilfe derer Eingaben, Ausgaben und interne Zustände des Testlings durch First-Order Formeln ersetzt werden, welche Eingabe-, Ausgabe- und Zustandsklassen identifizieren. Als zusätzliche Herausforderung werden wir POT im Zusammenhang mit autonomen Systemen studieren. Da POT enge Verbindungen zu MBT besitzt, wird sich ein unterstützendes Arbeitspaket mit vollständigen Modell-basierten Testtheorien für Systeme mit unendlichen Domänen für Eingaben, interne Zustände und Ausgaben befassen. Ein weiteres Arbeitspaket untersucht die Problematik konfigurierbarer Systeme, wie man sie im Product Line Testing vorfindet, und die existierende Äquivalenzklassentheorie auf konfigurierbare Parameter erweitern. Die CPOT-SM Forschungsergebnisse werden als experimenteller Prototyp in einem heute bereits industriell eingesetzten Werkzeug implementiert. Die ausgearbeiteten Methoden werden in diesem Framework anhand von Fallstudien validiert, welche wir mit internationalen Kooperationspartnern durchführen. Die Fallstudien decken die Gebiete Luftfahrtsteuerungssysteme, Bahnsteuerungen, autonome Fahrzeuge und Robotik ab.

• DFG-Verfahren: Sachbeihilfen