Temporallogische Laufzeitprüfung
Temporallogische Laufzeitprüfung
| Typ: |
Seminarthema |
| Betreuer: |
Daniel Bruns |
|
|
Beim Spezifizieren von Programmen werden Methoden typischerweise mit Vor- und Nachbedingungen versehen.
Dies erlaubt jedoch nicht temporale Aussagen wie "Methode x wird irgendwann in der Zukunft aufgerufen", die für die Verifikation von Sicherheitseigenschaften benötigt werden.
Mit "temporaljmlc" stellten Hussain und Leavens ein Werkzeug zur Laufzeitprüfung auf der Konferenz "Software Engineering and Formal Methods" (SEFM 2010) vor.
Die Spezifikationen sind in einer Variante der Java Modeling Language (JML) geschrieben, die um die aus der linearen temporalen Logik (LTL) bekannten Operatoren erweitert wurde.
temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking Temporal Properties
(IEEE International Conference on Software Engineering and Formal Methods, 2010, Paper)
