Inhalt

Model-Checking ist ein automatisches Verfahren für die Validierung von Modellen. Das Werkzeug JavaPathfinder überträgt Model-Checking-Techniken auf Java-Programme und kann diese gegen -- sehr einfache -- Eigenschaften validieren. In dieser Diplomarbeit soll JavaPathfinder erweitert werden, um auch Eigenschaften wie etwa "Beim nächsten Erreichen dieser Stelle gilt ..." oder "Wenn diese Zeile ausgeführt wird, gilt, dass die Methode X früher oder später aufgerufen wird" zu erschließen. Dazu sollen eine einfache Sprache definiert werden, in der sich solche Eigenschaften präzise erfassen lassen, und der Model-Checking-Algorithmus von JavaPathfinder entsprechend angepasst werden.

Voraussetzung

• Sehr gute Java-Programmierung
• Kenntnisse temporaler Logik
  

Aufgabensteller

Prof. Dr. Alexander Knapp

Betreuer

Gefei Zhang , Moritz Hammer