Logic and Formal Methods

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.