Home | deutsch  | Legals | Sitemap | KIT

Design and Implementation of a Verification Framework for Java Bytecode using Unstructured Dynamic Logic

Design and Implementation of a Verification Framework for Java Bytecode using Unstructured Dynamic Logic
Type:Diplomarbeit
Date:Mai 2012
Supervisor:

Prof. Dr. P. H. Schmitt
Mattias Ulbrich

Author:

Timm Felden

Beschreibung

In den letzten Jahren haben sich Spezifikations- und Verifikationstechniken für objektorientierte Systeme rasant weiterentwickelt. Wir wollen diese Entwickling vorantreiben, indem verschiedene Ergebnisse synergetisch gebündelt werden: 

Ihre Aufgabe in dieser Arbeit ist es, eine Ubersetzung für Programme der Programmiersprache Java in die Zwischensprache des Verifikationswerkzeugs ivil (beschrieben in [3]) zu übersetzen. Die Programme sollen dabei mit Spezifikationen in JML∗ (beschrieben in [4]) annotiert werden können.

Das interaktive Deduktionswerkzeug ivil, das am Insitut entwickelt wird, erlaubt die Verifikation von Programmen, die in einer speziellen Verifikations-Zwischensprache formuliert sind. JML∗ ist eine Erweiterung der Java Modelling Language JML [2] um “Dynamic Frames” [1], einem vielversprechendes Konzept zur Beschreibung von Auswertungs-Abhängigkeiten in objektorientierten Systemen.

In der Arbeit soll ein Konzept entworfen werden, wie JML∗ in möglichst großem Umfang zusammen mit Java Bytecode effizient in der Zwischensprache modelliert werden kann. Eine Implementierung soll erstellt werden, die diese Ubersetzung automatisch durchführt.

Literatur

[1] I. T. Kassios. The dynamic frames theory. Formal Aspects of Computing, 2010. To appear.
[2] G. Leavens, E. Poll, C. Clifton, Y. Cheon, and C. Ruby. Jml reference manual (draft).
[3] Mattias Ulbrich. A dynamic logic for unstructured programs with embedded assertions. In Bernhard Beckert and Claude Marché, editors, Proceedings, Formal Verification of Object-Oriented Software (FoVeOOS 2010), LNCS. Springer. To appear.
[4] Benjamin Weiß. Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. PhD thesis, Karlsruhe Institue of Technology, 2010.