Entwurf eines sprachunabhängigen Verifikationssystems auf der Basis denotationaler Semantikbeschreibungen

Meer over het boek

Mit dem zunehmenden Einsatz von Software in sicherheitsrelevanten Anwendungen wächst der Bedarf an Prüfmethoden, die über herkömmliches Testen hinausgehen. In dieser Arbeit wird ein System zur Prüfung von Programmen mit Zusicherungen entwickelt, dessen Kern konstant bleibt und dessen sprachspezifische Anteile aus der Sprachbeschreibung zur Compilererstellung generiert werden können. Die Grundidee besteht darin, Programme einer bestimmten Programmiersprache in eine Zielsprache zu übersetzen, das Zielprogramm zu prüfen und die Ergebnisse rückzuübersetzen. Ein zentraler Aspekt ist die Einführung eines speziellen Begriffs der Beweisprüfung, der nicht nur das Endergebnis, sondern auch Zwischenergebnisse liefert. Hierfür wird eine Spezialisierung des üblichen Termbegriffs über einer heterogenen Algebra entwickelt, die die Annotation von Zwischenergebnissen am Syntaxbaum ermöglicht. Zudem wird ein Kalkülbegriff entwickelt, der das Anhängen dieser Ergebnisse an den Syntaxbaum realisiert. Es wird erläutert, unter welchen Bedingungen diese Beweis(zwischen)ergebnisse in Bezug zum ursprünglichen Quellprogramm gesetzt werden können. Außerdem wird die Integration des Beweissystems in eine Programmierumgebung skizziert. Um die Anwendbarkeit des Konzepts zu demonstrieren, werden eine Beispiel-Zielsprache und ein Kalkül vorgestellt, die auf erweiterte typisierbare Lambda-Terme basieren, die auch in der Semantikdefinition von Programmiersprache