Zusammenfassung

Ralf Kneuper: Validation und Verifikation von Software durch symbolische Ausführung

in: P. Liggesmeyer, H.M. Sneed, A. Spillner: Testen, Analysieren und Verifizieren von Software.
Springer-Verlag 1992.

Die Grundidee der symbolischen Ausführung ist es, ein Programm auszuführen, ohne Werte für die Eingabevariablen anzugeben. Auf diese Weise erhält man ein Verfahren zur Validation und Verifikation von Programmen, das zwischen formalem Korrektheitsbeweis und Testen liegt.

Als Ausgabe der symbolischen Ausführung erhält man einen Term, der die Eingabevariablen als freie Variablen enthält. Man spricht dann von symbolischen Ein- und Ausgabewerten, die aus Variablen oder Termen anstelle konkreter Werte bestehen und auf diese Weise einen ganzen Bereich konkreter Werte abdecken.

Es gibt eine ganze Reihe verschiedener Ansätze, diese Methode der symbolischen Ausführung zur Validation und Verifikation von Programmen einzusetzen. Dieser Beitrag gibt einen Überblick über diese Ansätze, die dabei auftretenden Probleme, und Ansätze zu ihrer Lösung.