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

• Erstellungsjahr: 2024

Zusammenfassung der Projektergebnisse

Das Hauptziel dieses Projektes bestand in der Bereitstellung vollständiger Testmethoden (diese bieten Korrektheitsgarantien für Implementierungen, welchedie Tests bestehen), um zu verifizieren, dass Implementierungen ihre spezifiziertenEigenschaften erfüllen (sog. Eigenschafts-basiertes Testen., engl. propertyorientedtesting (POT)). Die Automatisierung von POT bei gleichzeitiger Zusicherungvon Vollständigkeit ist für die Verifikation sicherheits-kritischer Systemevon erheblicher Bedeutung, da dort die Stärke der durchgeführten Testsuitennachgewiesen werden muss, und Testkampagnen mit konventionellen Technikenunannehmbar aufwändig werden. Das Komplexitätsproblem, welches oft die praktische Anwendbarkeitvollständiger Test Suiten verhindert, wurde in diesem Projekt durch die Entwicklungsymbolischer Systemrepräsentationen gemindert, welche auf neuartigen Typenvon Äquivalenzklassen beruhen. Mithilfe dieser Klassen kann das Verhaltensmodelleiner Implementierung auf handhabbare Größe abstrahiert werden,ohne die Fähigkeit zu verlieren, alle Verletzungen der spezifizierten Eigenschaftenaufzudecken. Für zwei komplementäre POT Ansätze wurden neue vollständige Methodenentwickelt. Beide sind in der Lage, Implementierungen realistischer Komplexitätzu prüfen, wie man sie beispielsweise bei Airbag-Steuerungen, Geschwindigkeits-überwachungssystemen und Zugsicherungssystemen findet. Der erste Ansatzist für Entwicklungen nach dem Paradigma des model-based systems andsoftware engineering anwendbar, bei dem Entwurfsmodelle zusätzlich zu den gefordertenEigenschaften erzeugt werden. Die Verfügbarkeit eines die Eigenschaftenerfüllenden Modells ermöglicht es, die Eigenschaftserfüllung mit deutlich wenigerTestfällen nachzuweisen. Der zweite Ansatz ist auf Software-Modultestsspezialisiert und verwendet maschinelles Lernen, um automatisch eine Modellrepräsentation zu erstellen, welche dann mittels Modellprüfung bzgl. Eigenschaftserfüllung verifiziert wird. Ein quelloffenes Software Ecosystem wurde geschaffen, welches beideAns¨atze zum Eigenschafts-basierten Testen implementiert. Die Testerzeugung und -ausführung ist auf einer Cloud Server Farm möglich und frei verfügbar zuForschungs- und Evaluierungszwecken.

Projektbezogene Publikationen (Auswahl)

• New Distribution Paradigms for Railway Interlocking. Lecture Notes in Computer Science, 434-448. Springer International Publishing.
  Peleska, Jan
  
• Efficient data validation for geographical interlocking systems. Formal Aspects of Computing, 33(6), 925-955.
  Peleska, Jan; Krafczyk, Niklas; Haxthausen, Anne E. & Pinger, Ralf
  
• Exhaustive Property Oriented Model-Based Testing with Symbolic Finite State Machines. Lecture Notes in Computer Science, 84-102. Springer International Publishing.
  Krafczyk, Niklas & Peleska, Jan
  
• Effective grey‐box testing with partial FSM models. Software Testing, Verification and Reliability, 32(2).
  Sachtleben, Robert & Peleska, Jan
  
• libfsmtest An Open Source Library for FSM-Based Testing. Lecture Notes in Computer Science, 3-19. Springer International Publishing.
  Bergenthal, Moritz; Krafczyk, Niklas; Peleska, Jan & Sachtleben, Robert
  
• Model-Based Conformance Testing and Property Testing With Symbolic Finite State Machines - Technical Report. October 2022
  Wen-ling Huang, Niklas Krafczyk & Jan Peleska
  
• An Optimised Complete Strategy for Testing Symbolic Finite State Machines. Lecture Notes in Computer Science, 55-71. Springer Nature Switzerland.
  Huang, Wen-ling; Krafczyk, Niklas & Peleska, Jan
  
• Complete Property-Oriented Module Testing. Lecture Notes in Computer Science, 183-201. Springer Nature Switzerland.
  Brüning, Felix; Gleirscher, Mario; Huang, Wen-ling; Krafczyk, Niklas; Peleska, Jan & Sachtleben, Robert
  
• Efficient Gray Box Checking for C/C ++ Modules - Technical Report. Publisher: Zenodo, March 2024.
  Felix Brüning, Mario Gleirscher, Wen-ling Huang, Krafczyk Niklas, Jan Peleska & Robert Sachtleben
  
• Exhaustive property oriented model-based testing with symbolic finite state machines. Science of Computer Programming, 231, 103005.
  Huang, Wen-ling; Krafczyk, Niklas & Peleska, Jan