Zustandsfolgenbasierte Programmverifikation
| Typ: | SA |
|---|---|
| Datum: | 13.02.2012 |
| Betreuer: | Daniel Grahl |
| Aushang: |
Spezifikation und Verifikation von Programmen sind weitgehend zustandsbasiert: Man trifft Aussagen indem man die möglichen Anfangs- und Endzustände eines Programmes in Beziehung setzt. Dieses Verfahren hat zu mächtigen Verifikationssystemen wie KeY [1] geführt. Jedoch erweist sich die zustandsbasierte Sichtweise als nicht ausreichend sobald nebenläufige Prozesse betrachtet werden. Insbesondere wenn statt funktionaler Eigenschaften Sicherheitsaussagen wie die Vertraulichkeit von Geheimnissen benötigt werden, ist es notwendig, auch Zwischenzustände zu betrachten.
Die in [2] vorgestellte dynamische Logik basiert dagegen darauf, dass ein deterministisches Programm eine eindeutige Zustandsfolge von Zuständen repräsentiert. Auf dieser lassen sich dann temporale Aussagen treffen, wie etwa „x > 0 gilt solange bis y zugewiesen wurde“. Eine prototypische Implementierung in KeY liegt vor.
Im Rahmen dieser Studien- oder Bachelorarbeit soll die Brauchbarkeit dieser Methode untersucht werden. Dazu sollen zunächst Beispielprogramme entworfen und verifiziert wer- den. Zudem soll im Sinne der Benutzbarkeit auch eine Erweiterung der Java Modeling Lan- guage (JML) [3], einer verbreiteten Spezifikationssprache, erarbeitet werden, die temporale Methodenspezifikationen miteinschließt. (Es gibt ähnliche Ansätze dies mit dem Ziel der Laufzeitprüfung zu tun [4], wenn auch die dort verwendete Sprache minder aussagekräftig ist.)
Die Ausarbeitung in englischer Sprache ist erwünscht. Kenntnisse aus der Vorlesung Formale Systeme werden vorausgesetzt.
Literatur
- Bernhard Beckert, Reiner Hähnle, and Peter Schmitt, editors. Verification of Object-Oriented Software: The KeY Approach, volume 4334 of LNCS. Springer-Verlag, 2006.
- Bernhard Beckert and Daniel Bruns. Dynamic logic with trace semantics. Submitted to IJCAR, 2012.
- Gary T. Leavens and Yoonsik Cheon. Design by contract with JML. Draft, available from jmlspecs.org., 2005.
- Faraz Hussain and Gary T. Leavens. temporaljmlc: A JML runtime assertion checker extension for specification and checking of temporal properties. Technical Report CS-TR-10-08, UCF, Dept. of EECS, Orlando, Florida, July 2010.