Vortragender
|
Titel / Kurzfassung |
Egon Börger,
University of Pisa |
On the use of Gurevich's abstract state machines for modular development
of well documented formally inspectable software. A case study: The Steam-Boiler
control program.
Gurevich's abstract state machines (evolving algebras) have been used
to specify languages (e.g. Prolog, C++,VHDL) and architectures
(e.g. PVM, APE100, Transputer, DLX), to validate standard language
implementations (e.g. of Prolog, Occam), to verify numerous
distributed and real-time protocols, etc..
In this talk we explain the use the software designer can make of
Gurevich machines for a systematic modular development of well
documented programs which can be inspected using formal means. We
exemplify the method through the solution of the steam boiler problem
which has been developed jointly with C. Beierle, I. Durdanovic,
U. Glässer and E. Riccobene (see Springer LLNCS vol. 1165).
As starting point we present the ground model which faithfully
reflects the steam boiler control system (as informally specified by
J.-R. Abrial for the 1995 Dagstuhl workshop on the comparison of
specification methods). We explain how the information hiding
and abstraction mechanism of Gurevich machines allows the
designer to discuss and negotiate with the customer, in rigorous yet
simple terms of traditional mathematical language, in such a way that
they can come to a common understanding of the contract (i.e. on what
the informal description really means) and on its eventually being met
by the formal design.
Starting from this abstract model of the system we go through a number
of refinements all the way to a C++ program (which controls
successfully the steam-boiler environment implemented for the Dagstuhl
workshop by A. Lötzbeyer from FZI Karlsruhe). The ability of Gurevich
mqchines to reflect arbitrary abstraction levels facilitates the
modular development of different components and a transparent
definition of precise interfaces through which these components
are put together.
The various models allow us also to prove interesting properties of
the system at appropriate abstraction levels; this feature is crucial
for inexpensive and easy yet controlled extendability and
modifiability of the design.
|
|
Axel Dold, Universität Ulm |
Generische Spezifikation und Verifikation von Übersetzungsschritten
Die meisten der bisher dokumentierten Arbeiten zur
maschinell unterstützten Übersetzer-Spezifikation und -Verifikation
betreffen jeweils spezielle Quell- und Zielsprachen, so
dass eine Wiederverwendung fuer andere Übersetzungsprozesse kaum moeglich ist.
Andrerseits läuft die Übersetzung einzelner Sprachkonstrukte jeweils nach
einem Schema ab, das sich nur in Details von Sprache zu Sprache unterscheidet;
z.B. umfasst die Ubersetzung einer Zuweisung die Schritte Code-Erzeugung
für den Ausdruck, gefolgt von einer Abspeicherung des berechneten Werts.
Es liegt daher nahe, das Wesentliche solcher Übersetzungsmuster zu
identifizieren und abstrakt zu modellieren und zu verifizieren, so dass sie
in geeigneter Form fuer konkrete Übersetzungsprozesse instanziiert und
wiederverwendet werden können. Ein solches Vorgehen unterstuetzt ausserdem die
fuer die Durchfuehrbarkeit maschineller Beweise notwendige Modularisierung
des Übersetzungsprozesses.
In dem Vortrag werden beispielhaft generische Theorien zur Übersetzung
von Ausdruecken und darauf aufbauend fuer Kontrollstrukturen vorgestellt,
die von Details der Quellsprache und Architektur und Instruktionssatz der
Zielmaschine abstrahieren.
Wir zeigen, wie und in welchem Umfang ein solchen Ansatz sich im PVS-System
realisieren lässt und wie die abstrakten Theorien für die konkreten
Übersetzungsprozesse des Verifix-Projektes eingesetzt werden können.
|
|
Thilo Gaul, Universität Karlsruhe |
Beweis der lokalen Korrektheit termersetzungssystembasierter
Codeerzeugung
Soll ein Softwaresystem verifiziert implementiert werden, muß
entweder direkt auf Ebene der Zielmaschine überprüft werden,
oder aber ein verifizierter Übersetzer füe die eingesetzte
Hochsprache vorhanden sein. Unser Ziel ist es, verifiziert
implementierte Übersetzer zu konstruieren, die effizienten Code
fü gängige Sprache erzeugen. Der Codegenerator ist
gemäß unserer Architektur der Teil eines Übersetzers,
der die Transformation in konkrete Maschineninstruktionen vornimmt.
Sollen praktisch relevante Übersetzer konstruiert werden,
müssen auch praktisch erprobte und effiziente Verfahren
eingesetzt werden. Dies betrifft sowohl Optimierungstechniken als auch
die Transformationsschritte selber.
Im Übersetzerbau haben sich Termersetzungssysteme als Mechanismus
fü diesen Transformationsschritt bewährt. Neben globalen
Bedingungen an das Termersetzungssystem (siehe Zimmermann)
fallen bei der Verifikation einzelner Ersetzungsregeln lokale
Beweisverpflichtungen an. Diese sind hochgradig sprachabhängig,
fallen in großer Anzahl an und sind zudem sehr
fehleranfällig. Wir zeigen, wie diese Regeln systematisch durch
Simulationsbeweise verifiziert werden können und wie mechanische
Beweisunterstützung Fehler finden hilft, und geben einige Beispiele.
|
|
Wolfgang Goerigk, Universität Kiel |
Der ACL2-Korrektheitsbeweis eines einfachen Theorembeweisers
ComLisp, eine applikative Teilsprache von Common Lisp mit imperativen
Bestandteilen, Zuweisung, sequentieller Komposition und Schleifen, ist
sorgfältig gewählte Quell- und Übersetzer- oder
Systemimplemetierungssprache in Verifix. Der applikative Teil findet
sich auch in der Logik des neuen Boyer-Moore-Theorembeweisers ACL2
wieder. Der Vortrag zeigt, wie ACL2 mechanische Korrektheitsbeweise
für applikative ComLisp-Programme erlaubt. Totaler
Korrektheitsbeweis in ACL2-Logik geht ohne weitere
Beweisverpflichtungen in partiellen Korrektheitsbeweis für das
ComLisp-Programm über, Erhalten partieller Korrektheit als
Implementierungsbegriff überträgt schließlich
partielle Korrektheit auf das binäre ausführbare
Maschinenprogramm, von dem somit nachgewiesen ist, daß im Falle
regulären Terminierens das Resultat korrekt im Sinne des
Quellprogrammes ist, daß der Benutzer sich auf die Resultate von
Programmläufen verlassen kann. Als Fallstudie wählen wir
einen kleinen Theorembeweiser, eine Entscheidungsprozedur für
aussagenlogische Tautologien.
|
|
Gerhard Goos, Universität Karlsruhe |
Eine Architektur zur Konstruktion korrekter Übersetzer
Verifizierte Übersetzer sind essentiell für die Entwicklung
sicherheistkritischer Softwaresysteme. Kritische Teile von
Steuersystemen werden immer noch auf Assemblerebene geschrieben und
verifiziert, da Übersetzer für Hochsprachen nicht als
vertrauenswürdig angesehen werden. Für industrielle
Anwendungen müssen die Techniken zur Konstruktion korrekter
Übersetzer einfach anzuwenden und in den
Softwareentwicklungsprozeß einzubinden sein. So entstehen nicht
nur algorithmische Probleme der Verifikation, sondern auch
Architekturprobleme der Konstruktion verifizierter Übersetzer
gemäß aktueller Softwareentwicklungsstandards. Wir zeigen,
daß Spezifikation und Verifikation in die traditionelle
Übersetzerarchitektur integriert werden können. Diese
Integration reduziert sowohl die Komplexität, als auch den Umfang
der Verifikation.
|
|
Andreas Heberle, Universität Karlsruhe |
Konstruktion eines korrekten Übersetzers einer while-Sprache
Am Beispiel der verifizierten Übersetzung einer einfachen
While-Sprache stellen wir eine Instanziierung der Architektur zur
Konstruktion verifizierter Übersetzer vor. Die Zielsprache ist dabei
eine Teilmenge des DecAlpha Maschinenkodes. Es zeigt sich, daß die
Übersetzungsspezifikation auf natürliche Art und Weise entsprechend
der traditionellen Übersetzerstruktur aufgeteilt werden kann. Eine
weitere Verfeinerung der Spezifikation und Implementierung führt zu
Modulen, die für jeden Übersetzer, die nur ein einziges Mal oder die überhaupt
nicht verifiziert werden müssen.
Trotz der einfachen Quell- und Zielsprache behandelt die Übersetzung
viele praktisch relevante Probleme, z.B. wird explizit eine
Zwischensprache eingeführt und es wird auf die Korrektheit der
Registerallokation und der Adressrechnung eingegangen.
|
|
Friedrich von Henke, Universität Ulm |
Formale Spezifikation und Verifikation in der
Entwicklung verifizierter Übersetzer
Bei der Entwicklung verifizierter Übersetzer fallen eine Vielzahl von
Modellierungs-, Spezifikations- und Beweisaufgaben an, die ohne maschinelle
Unterstützung nur schwer zu bewältigen sind, wenn der Anspruch auf formal
begründete und nachvollziehbare Schritte erfüllt werden soll.
Es ist ein formal-logischer Rahmen erforderlich, der einerseits die für die
Modellierung von Sprachen und Zielmaschinen und deren Semantik notwendige
Ausdruckskraft bereitstellt, andrerseits auch genügende Unterstützung für
deren Analyse, insbesondere die Entwicklung formaler Beweise, bietet, so dass
die gesamte formale Entwicklung in einem einheitlichen, maschinell gestützten
logischen Kontext geschieht. Aus pragmatischen Gründen wird im Verifix-Projekt
für diese Aufgabe PVS eingesetzt. Anhand von typischen Beispielen illustrieren
wir Modellierung und Beweis in PVS und zeigen, inwieweit PVS den Anforderungen
gerecht wird, die sich bei der Entwicklung verifizierter Übersetzer ergeben.
|
|
Ulrich Hoffmann, Universität Kiel |
Implementierungsverifikation für den initialen
ComLisp-Übersetzer auf dem Transputer
Die Struktur des initialen, korrekt und korrekt implementierten
Übersetzers paßt sich in die Architektur zur
Konstruktion korrekter Übersetzer ein. Die Übersetzung
ist in 4 Schritte eingeteilt; 3 Zwischensprachen SIL, Cint und TASM
sind dazu definiert worden. Ausgehend von korrekten
Übersetzungsspezifikationen werden Übersetzerprogramme in
der Quellsprache, hier ComLisp, selbst korrekt konstruiert. Durch einen
Bootstrap mit anschließendem Beweis durch Probe
kann die korrekte Implementierung des Übersetzers auch im
Maschinencode, hier dem des Transputers, bewiesen werden.
|
|
Hans Langmaack, Universität Kiel |
Starker Übersetzertest als relevanter Bestandteil vollen
Übersetzerkorrektheitsbeweises.
Um einen Übersetzer für eine höhere Programmiersprache PL auf einer
Zielmaschine TM zu implementieren, empfiehlt sich das Bootstrapping
mit vorhandenem unverifizierten Übersetzer für eine Obersprache PL0
auf einem Wirtprozessor HM0. Wegen dieses Univerifiziertseins
sollte man den sog. starken Übersetzertest durchführen. Durch
Einschleusen von Viren kann der Test aber von einem versierten Hacker
überlistet werden. Ein Implementierungskorrektheitsbeweis hätte die
Viren aufgedeckt. Im Sinne der Theorie der Testdatenselektion von
J.B. Goodenough und S.L. Gerhart genügt aber ein eingeschränkter
Beweis, um trotzdem volle Übersetzerkorrektheit zu garantieren.
|
Motivation und Ziele für das Projekt Verifix
Obwohl Programmiersprachen und Übersetzerkonstruktion diejenigen
Teilgebiete der praktischen Informatik sind, deren Theorien am besten
erforscht sind, kann man sich auf Übersetzer immer noch nicht voll
verlassen, insbesondere nicht bei realistisch-industriell eingesetzten
Programmiersprachen auf realen Prozessoren.
Zwei Gründe sind hauptverantwortlich:
Die Literatur zur Übersetzerverifikation diskutiert nur die
Korrektheit von Übersetzungsspezifikationen, wie die ebenso
erforderliche Korrektheit von Übersetzerimplementierungen bis hinab
zum binären Maschinencode. Diese Literatur geht auch nicht auf die
traditionell benutzten Architekturen realistischer Übersetzer und
Übersetzergeneratoren ein. Mit Blick auf realistische, industrielle
Anwendung sucht Verifix diese Lücken zu beseitigen, so daß künftig
auch in sicherheitskritischen Fällen kein niederer Code mehr
inspiziert werden muß.
|
|
Markus Müller-Olm, Universität Kiel |
Modulare Übersetzungs-Verifikation
In zunehmendem Maße wird Software auch in sicherheitskritischen
Systemen eingesetzt. Damit stellt sich die Frage nach der Korrektheit
der bei der Softwareentwicklung verwendeten Werkzeuge. Insbesondere
gilt dies für die benutzten Übersetzer; ist deren Korrektheit
gesichert, so kann die Zertifizierung der sicherheitskritischen
Software auf Quellcodeniveau durchgeführt werden. Dies verspricht
effektiver zu sein als die gängige Praxis, den generierten Code zu
analysieren.
Die Literatur über Compiler-Verifikation beschaeftigt sich allerdings
meist nur mit der Übersetzung auf idealisierte Maschinen. Ich werde
über die korrekte Konstruktion einer Übersetzungsvorschrift auf
einen realen Prozessor (den inmos-Transputer) berichten. Die
Quellsprache ist eine prototypische Echtzeitprogrammiersprache
(while-Programme mit Blöcken, Kommunikation und oberen Schranken für
Ausführungszeiten von Basisblöcken). Kontext ist das von der EU von
1992--1995 geförderte ESPRIT Projekt ProCoS II (Provably Correct
Systems II), das sich mit korrekter Konstruktion von Software für
eingebettete Systeme beschäftigte.
Bei der korrekten Konstruktion von Übersetzern auf reale Prozessoren
muß man eine Vielzahl von z.T. Prozessor-spezifischen Details
behandeln. Von besonderer Wichtigkeit ist daher ein modulares
Vorgehen, das sowohl das Erstellen des Beweises als auch dessen
Kontrolle unterstützt. Ich werde zeigen, wie einzelne
Quellprogrammkonstrukte, einzelne Instruktionen des Zielprozessors,
sowie einzelne Teilaspekte der Übersetzung in einem konsistenten
Rahmen unabhängig voneinander behandelt werden können.
|
|
Holger Pfeifer, Universität Ulm |
Mechanisierte Semantik von Programmiersprachen
Bei der Semantik von Programmiersprachen werden traditionell drei
Formen unterschieden: denotationelle Semantik, operationelle Semantik
und axiomatische Semantik. Die verschiedenen Formen von Semantik sind
für unterschiedliche Anwendungen geeignet: z.B. eine operationelle Semantik
als Grundlage für die Implementierung einer Sprache und axiomatische oder
denotationelle Semantiken zur Unterstützung von Verifikationsaufgaben.
Die Semantik-Formen stellen damit keine Alternativen dar, sondern ergänzen
sich hinsichtlich ihrer Haupt-Anwendungsbereiche. Es ist daher sinnvoll,
für eine Programmiersprache miteinander konsistente Formen der Semantik zu
entwickeln.
Im Rahmen des Verifix-Projekts wurde eine formale generische Modellierung der
Semantik-Formen für gängige Programmiersprachkonstrukte zusammen mit den
zugehörigen mathematischen Grundlagen im Spezifikations- und
Verifikationssystem PVS entwickelt. Diese Modellierung ermöglicht es,
in einem einheitlichen formalen Rahmen die Beziehungen zwischen den
Semantik-Formen abzuleiten, so dass anschliessend etwa zum Beweis von
Eigenschaften einer operationellen Semantik eine denotationelle Semantik,
die von irrelevanten Details abstrahiert, herangezogen werden kann.
Wir stellen diese Modellierung vor als Grundlage für die im Verifix-Projekt
anfallenden Modellierungs- Verifikationsaufgaben.
|
|
Wolf Zimmermann, Universität Karlsruhe |
Die Korrektheit der Simulationsbeweistechnik für
Übersetzer-Backends
Übersetzer Codegeneratoren übersetzen Programme aus
niedrigen Zwischensprachen in äquivalente Maschinenprogramme. Wir
definieren die Korrektheit dieser Übersetzung basierend auf
operationalen Semantiken der Zwischen- und Maschinensprache, wobei die
Übersetzungsspezifikation durch eine Menge von Termersetzungsregeln
gegeben ist. Der Vortrag zeigt, daß alle Codegeneratoren, die durch
ein Termersetzungssystem erzeugt wurden, korrekt sind, wenn der
Codegenerator-Generator, Registerzuteiler, sowie die
Termersetzungsregeln bestimmten Anforderungen genügen. Die
Anforderungen an die einzelnen Termersetzungsregeln sind
unabhängig von den restlichen Termersetzungsregeln und bestehen
aus Einzelsimulationen, die zu einem Simulationsbeweis zusammengesetzt
werden können. Die Korrektheit des Codegenerator-Generators und die
Anforderungen an den Registerzuteiler sind unabhängig von den
beteiligten Sprachen und sind nur mit Zwischensprache und
Maschinensprache parametrisiert. Zur Konstruktion korrekter
Übersetzer genügt es demnach, diese beiden Aufgaben
insgesamt aus einer korrekten Bibliothek zu entnehmen, die für
alle Codegeneratoren verwendet werden kann. Um einen neuen korrekten
Codegenerator zu konstruieren, reicht es aus die Anforderungen an die
einzelnen Termersetzungsregeln zu beweisen und den
Codegenerator-Generator und Registerzuteiler aus der Bibliothek
geeignet zu parametrisieren. Der Vortrag von T. Gaul führt anhand
einzelner Beispiel solche Beweise durch.
|
