Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Modular Verification of JML Contracts Using Bounded Model Checking

Typ: MA
Datum: 2017-07-14
Betreuer: Mattias Ulbrich
Michael Kirsten
Aushang:

Ziel

In Kooperation mit der Technischen Universität Darmstadt sowie der Technischen Hochschule Chalmers entwickelt unser Lehrstuhl das Software-Verifikations-Werkzeug KeY, mit dem die formale Korrektheit von Java-Programmen bezüglich gültiger JML-Verträge mittels eines logischen Beweiskalküls interaktiv bewiesen werden kann. Der Regelsatz von KeY unterstützt hierzu einige Datentypen, die für einen formalen Beweis in logische Formeln überführt werden.

Allerdings gibt es auch Datentypen wie beispielsweise Bit-Vektoren, bei denen andere explorierende Techniken geeigneter scheinen. Außerdem können Beweise in KeY bisweilen sehr aufwändig und unübersichtlich werden. Hier erscheinen automatische, aber weniger mächtige, Beweistechniken vielversprechend, die Teile des Beweises zu übernehmen, die ohne Nutzerinteraktion auskommen oder um schnell Gegenbeispielen zu generieren.

Innerhalb dieser Abschlussarbeit soll nun ein Konzept untersucht und implementiert werden, um Beweisverpflichtungen für Bit-Vektor-Variablen und andere "automatische" Aufgaben aus KeY zu extrahieren und hierfür einen bounded model checker (z. B. Java Pathfinder oder CBMC) zu beauftragen, der gut damit umgehen kann. Anschließend soll das Ergebnis wieder von KeY verarbeitet oder mit den restlichen mittels KeY gewonnenen Ergebnissen zu einem Gesamtergebnis übersetzt werden können. Insbesondere sollen in der Spezifikationssprache Java Modeling Language (JML) spezifizierte Kontrakte für eine modulare Kommunikation genutzt werden.

Kontakt: