Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25991
Titel: Compiler verification in the context of pervasive system verification
Verfasser: Leinenbach, Dirk Carsten
Sprache: Englisch
Erscheinungsjahr: 2008
SWD-Schlagwörter: Verifikation
Codegenerierung
Algorithmus
Compiler
Freie Schlagwörter: C0
VAMP Assembler
verification
compiling specification
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: This thesis presents the formal verification of the compiling specification for a simple, non-optimizing compiler from the C-like programming language C0 to VAMP assembly code. The main result is a step-by-step simulation theorem between C0 programs and the compiled code (which is specified by the compiling specification). Additionally, a C0 small-step semantics and a verification methodology for VAMP assembly have been developed. This work is part of the Verisoft project which aims at the pervasive formal verification of an entire computer system. The key concept in Verisoft';s methodology is to prove properties of computer systems at the relatively abstract C0 layer and to transfer them via several intermediate layers down to the concrete hardware layer. After successful transfer of a property to the hardware layer, we can be sure that no oversimplifications have been done in the formalizations of the more abstract layers. This context of pervasive system verification imposes several special requirements to our compiler correctness theorem. In particular, the simulation theorem had to be formulated based on small-step semantics to allow for reasoning about non-terminating and interleaving programs. Another important feature is that our result incorporates resource restrictions at the hardware layer and allows to discharge them at the C0 layer. All results presented in this thesis have been formalized in the theorem prover Isabelle / HOL.
Die vorliegende Arbeit befasst sich mit der formalen Verifikation des Codegenerierungsalgorithmus eines nicht optimierenden Compilers von der C-ähnlichen Sprache C0 nach VAMP Assembler. Das Hauptergebnis ist ein Schritt-für- Schritt Simulationssatz zwischen C0 Programmen und dem compilierten Code. Die Arbeit umfasst zus¨atzlich die Entwicklung einer Small-Step Semantik für C0 sowie einer Verifikationsmethodik für VAMP Assemblerprogramme. Diese Arbeit ist Teil des Verisoft Projekts, das auf die durchgängige formale Verifikation von Computersystemen abzielt. Die Methodik von Verisoft basiert auf der Verifikation von Eigenschaften eines Computersystems auf der relativ abstrakten C0 Ebene und deren anschließendem Transfer auf die konkrete Hardwareebene. Ein solcher erfolgreicher Eigenschaftstransfer garantiert, dass auf den abstrakten Ebenen keine zu starken Vereinfachungen vorgenommen worden sind. Die Einbettung in die durchgängige Verifikation von Systemen stellt zahlreiche speziellen Anforderungen an den Compilerkorrektheitssatz. Insbesondere muss der Simulationssatz auf einer Small-Step Semantik basieren, um die Behandlung von nebenläufigen und von nicht terminierenden Programmen zu ermöglichen. Eine weitere Eigenschaft ist, dass unser Resultat Ressourcenbeschränkungen auf der Hardwareebene einbezieht und deren Entlastung auf der C0 Ebene erlaubt. Alle Resultate dieser Arbeit sind im Theorembeweiser Isabelle / HOL formalisiert worden.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-32409
hdl:20.500.11880/26047
http://dx.doi.org/10.22028/D291-25991
Erstgutachter: Paul, Wolfgang J.
Tag der mündlichen Prüfung: 24-Jun-2008
SciDok-Publikation: 2-Aug-2010
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
Dissertation_6767_Lein_Dirk_2008.pdf2,4 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.