Vortragender
|
Titel / Kurzfassung |
| Gerhard Goos,Universität Karlsruhe |
Verifix: Projekt, Ziele, Ergebnisse
Zusammenfassung ...
|
|
Wolf Zimmermann, Universität Karlsruhe |
ASM's: Spezifikation dynamischer Semantik und Simulation
Der Vortrag gibt einen Überblick über die Definition von Semantiken mit Abstrakten
Zustandsmaschinen (ASMs) und Montages, diskutiert die Vorgehensweise bei der Verifikation
der Transformation, und skizziert einzelne Simulationsbeweise. Zunächst werden aus den
Anforderungen für Verifix Anforderungen an Semantikstile abgeleitet. Es wird gezeigt,
daß ASMs sehr gut geeignet zur Spezifikation der Semantik von Maschinensprachen und
Zwischensprachen ist, während beispielsweise denotationale Semantik und strukturell
operationale Semantik für diesen Zweck ungeeignet ist. Da mit Montages eine
kompositionale Spezifikationstechnik zur Definition von ASMs für höhere
Programmiersprachen existiert, sind ASMs eine geeignete Wahl.Anschließend wird
gezeigt, wie man methodisch die Semantiken für Maschinensprachen,
Zwischensprachen und Quellsprachen definiert.
Basierend auf solchen Semantikdefinitionen werden dann die Transformationen
verifiziert. Dazu bildet man zunächst den
Speicherzustandsraum der Quellsprache (Zwischensprache) auf den
der Zwischensprache (Zielsprache) ab, anschließend können die beteiligten Sprachen
vereinigt werden und auf dieser Basis die Transformationen bewiesen werden, und
schließlich wird der Befehlszeiger der Quellsprache (Zwischensprache)
auf den Befehlszeiger der Zwischensprache (Zielsprache) abgebildet.
Der Vortrag zeigt für jeden
dieser Schritte die notwendigen Beweisverpflichtung und
führt exemplarisch solche Beweise vor.
|
|
Andreas Heberle, Universität Karlsruhe |
Transformationsverifikation
Der Vortrag diskutiert den Zusammenhang zwischen der operationellen
Semantikspezifikation von Quellsprachen mit Montages und den
Beweisverpflichtungen zum Nachweis der Korrektheit von
Übersetzungen. Wir geben eine Konstruktionsmethode an, mit der aus dem
Nachweis der lokalen Korrektheit von Übersetzungen von
Sprachkonzepten auf die globale Korrektheit geschlossen werden
kann. Damit ergibt sich eine Modularisierung des Korrektheitsbeweises
für die Transformationsphase.
Zusätzlich diskutieren wir Wiederverwendungsfragen und stellen einen
Kalkül für korrekte Übersetzungen vor. Der Kalkül stellt im Prinzip
eine Bibliothek von Sprachkonzepten zusammen mit korrekten
Übersetzungen dar. Definiert man die Semantik einer Quellsprache durch
Abbildung in die Sprache des Kalküls, dann können sowohl Semantik von
Sprachkonzepten als auch korrekte Transformationen wiederverwendet
werden. Der Kalkül ist durch eine objekt-orientierte Bibliothek
implementiert. Implementierungskorrektheit ergibt sich durch
korrekte Komposition von beschränkten generischen Klassen, die
Sprachkonzepte repräsentieren, und Standardprogrammverifikation von
Transformationen.
|
|
Ulrich Hoffmann, Universität Kiel |
Übersetzerimplementierungsverifikation
Zusammenfassung...
|
|
Wolfgang Goerigk, Universität Kiel |
Programmprüfung
In diesem Vortrag beschreiben wir die mathematischen Grundlagen
und Einsatzmöglichkeiten der Technik der Programmprüfung und
der checker-basierten Programmverifikation zur
Übersetzerverifikation im Rahmen des Verifix-Projektes.
Programmprüfung basiert auf Laufzeitprüfung von
Nachbedingungen eines Programms oder Programmteils durch
hinreichende algorithmische Formulierungen von
Korrektheitsprädikaten. Checker-basierte Programmverifikation
ist eine Technik zur vollen Verifikation der partiellen
Korrektheit, die Laufzeitprüfung ausnutzt und eine
Modularisierung des Programms in einen (häufig großen)
unkritischen Teil und kritische, zu verifizierende Prüfroutinen
erlaubt. Letztere lassen sich geradlinig induktiv formulieren
und leichter verifizieren.
In einem Beispiel zeigen wir im zweiten Teil Definition und
Verifikation der Korrektheit der Analysephase mit lexikalischer,
syntaktischer und semantischer Analyse auf der Basis von
Attributgrammatiken. Andere Beispiele auch außerhalb des
Übersetzerbaus werden kurz skizziert.
|
|
Thilo Gaul, Universität Karlsruhe |
Programmprüfung in Übersetzern und Übersetzergeneratoren
Übersetzerverifikation erfordert vor allem für praktische Quell- und
Zielsprachen den Korrektheistnachweis einer großen Menge
Beweisverpflichtungen. Den größten Anteil hieran haben
Implementierungsverifikationen, da auf Ebene der
Implementierungssprache klassische Programmverifikation betrieben
werden muß. Ziel der Programmprüfungsarbeiten im Verifix-Projekt ist
es, diesen Aufwand ganz erheblich zu reduzieren. Der Vortrag zeigt
eine Methode auf, die Gesamtkorrektheit der Implementierung eines
Übersetzers zu etablieren, die auf dem Einsatz korrekt konstruierter
Laufzeitprüfer basiert. Auf die in dem Vortrag von W. Goerigk gelegten
Grundlagen wird Bezug genommen.
Im Vortrag zeigen wir in einer Rechnerdemonstration einen laufenden
Übersetzer für unsere Beispielsprache IS, der durch Anwendung
der Programmprüfungsmethode verifiziert attibutierte Strukturbäume
liefert. Der Übersetzer selber wurde vollständig mit Hilfe der
COCKTAIL-Werkzeuge generiert, die Implementierung liefert eine
hocheffiziente Analysephase. In der Vorführung wird ebenfalls
demonstriert, daß fehlerhafte Implementierungen - hier absichtlich
herbeigeführte C- und Werkzeug-Fehler - sich auf keiner Ebene auf die
Gesamtkorrektheit der Übersetzung auswirken können.
|
|
F.W. von Henke, Universität Ulm |
Maschinell unterstützte Verifikation
Zusammenfassung...
|
|
A. Dold, Universität Ulm |
Maschinelle Verifikation von Übersetzungsprozessen
Dieser Vortrag gibt einen Überblick über die aktuellen Arbeiten im
Bereich maschinell-unterstützter Verifikation der Transformation
und Implementierung.
Wir stellen einen generischen Ansatz zur formalen Spezifikation und
Verifikation prozeduraler Programme vor, der von konkreten
Übersetzungsprozessen abstrahiert, indem das Wesentliche eines
Übersetzungsschrittes identifiziert und abstrakt modelliert wird.
Ein solcher Ansatz erlaubt eine für die Durchführbarkeit maschineller
Beweise adäquate vertikale und horizontale Modularisierung.
Der Ansatz wird mit Hilfe generischer PVS-Theorien für einzelne
Sprachkonstrukte und Übersetzungsschritte realisiert, die mit den jeweils
relevanten Komponenten des Übersetzungsschrittes parametrisiert sind.
Backend-Spezifikation bestehen aus einer Menge von Regelschemata, die
Zwischensprachtermen Zielcode zuordnen. Wir stellen vor, wie solche
Spezifikationen mit Hilfe spezialisierter PVS-Strategien vollautomatisch
formal verifiziert werden können.
Bei der Implementierungsverifikation verfolgen wir einen konstruktiven
Ansatz, bei welchem ein Übersetzerprogramm durch Anwendung
semantik-erhaltender
Transformationen aus der Übersetzungsspezifikation generiert wird.
Es wurde hierzu ein formaler Rahmen in PVS entwickelt, der die
Integration von
Entwicklungsschritten und Transformationen aus unterschiedlichen
transformationellen Ansätzen erlaubt.
Die Anwendung des formalen Rahmens wird am Beispiel der
Konstruktion eines Übersetzers von ComLisp nach SIL illustriert.
|
|
Hans Langmaack, Universität Kiel |
Erreichtes und Perspektiven
In der zweiten Zweijahresprojektphase ist Verifix einen überzeugenden
Schritt hin zu einer ingenieurmäßigen und industriell einsetzbaren
Technik zur Entwicklung und Konstruktion voll verifizierter,
realistischer Übersetzer und Übersetzergeneratoren für realistische
Programmiersprachen auf realen Prozessoren gelungen.
Volle Verifikation heißt, daß auch Übersetzer und
Übersetzergeneratoren, die als ablauffähige, binäre
Maschinenprogramme realer Prozessoren implementiert sind, lückenlos
als korrekt eingesehen und bewiesen werden können.
Hervorzuhebendes Verifix-Merkmal ist, daß praktisch-industriell
bewährte Entwicklungsmethoden für Übersetzer und Generatoren
beibehalten werden; die Verifikation wird in modular-additiver Weise
draufgesattelt. Das ist möglich geworden durch systematisches
Einsetzen der Idee der Programmprüfung (Beweis durch Probemachen,
result-checking, speziell sog. Codeinspektion).
In der Projektausschreibung "Werkzeug zur Analyse von Objectcode und
von optimierenden Übersetzern -- OCOCAT", 1996, hat das Bundesamt
für Sicherheit in der Informationstechnik BSI festgestellt:
Jedes Software-Herstellungsverfahren hat zwei Brüche
(Sicherheitslücken) in lückenloser, konsistenter Überprüfbarkeit:
Übergang von Softwareentwurf zu hochsprachlichem Quellcode, und von
dort zu integriertem, ablauffähigem, binärem Maschinencode.
OCOCATs Anliegen ist die Sicherheitslücke 2., d.h. das bisher nicht
erreichte, voll korrekte, realistische Übersetzen.
Das aber ist gerade auch das Anliegen von Verifix. Es ist bemerkenswert,
daß das BSI die Sicherheitslücke 2. jetzt anerkannt hat. Das war
vor zehn Jahren in der Definitionsphase des BSI-Projekts ``VSE --
Verification Support Environment'' noch nicht so, weshalb der
Vortragende mit seinen Vorschlägen damals nicht auf Resonanz beim BSI
gestoßen war.
Mit dem erfolgreichen Einsatz der Technik des Programmprüfens im voll
korrekten realistischen Übersetzerbau zeigt Verifix Perspektiven auf,
wie im generellen Softwareengineering existierende Software
weiterverwendet werden kann. Ferner ist hervorzuheben, daß
Programmiersprachen und Übersetzerbau dasjenige praktische
Informatikgebiet ist, das am stärksten von Theorie durchdrungen
ist. Die Mitstreiter in Verifix sind sich einig, daß vor allem
deshalb der Bau voll korrekter, realistischer, industrierelevanter
Übersetzersoftware gelingen kann. Es ist zu hoffen, daß auch anderen
praktischen Informatikbereichen eine ähnliche Durchdringung mit Theorie
gelingt.
|
