Veröffentlichung im Rahmen des 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'11) auf Schloss Raesfeld.

Abstract: Zur Software-Modell-Prüfung, zum modellbasierten Testen und bei der Testdaten- und Codegenerierung sind die Größe und Komplexität von Modellen entscheidende Einflussfaktoren. Aus Quellcode (z.B. C oder Java) gewonnene Modelle in Form von symbolischen Kellersystemen (SPDS) erlauben nicht nur präzisere Ergebnisse, sondern führen auch ohne Modellexplosion bei exakter Nachbildung von Rekursion zu weniger Fehlalarmen als die Modellprüfung endlicher Systeme. Derart gewonnene Modelle beschreiben allerdings viel unwichtiges Verhalten sehr detailliert, was den Zustandsraum unnötig vergrößert und damit Modell-Prüfung, Testen usw. erschwert. Eine Form zur Vermeidung dieses unwichtigen Verhalten in der Modellbeschreibung ist die Abstraktion. Dabei wird das Programm oder komplexe Modell in ein weniger detailliertes Modell überführt. Ziel dieser Arbeit ist es, unwichtige Teile der Modellbeschreibung eines SPDS durch gegebene temporale Formeln selektiv zu identifizieren und davon zu abstrahieren.

Download: kps11.pdf