Vierwertige Timed-LTL-Semantik

Zusammenfassung

Es soll eine vierwertige Semantik für die Timed Linear Temporal Logic entwickelt sowie ein passendes Automatenmodell, welches die Eigenschaften der Semantik wiederspiegelt, angegeben werden. Außerdem soll die Umwandlung der Formeln der neu entwickelten Semantik in das Automatenmodell in die Logik- und Automatenbibliothek RltlConv implementiert werden.

Beschreibung

Für die Verifikation von Programmen während der Laufzeit (Runtime-Verification, RV) wird eine Spezifikationssprache benötigt, mit der die zu überwachenden Eigenschaften angegeben werden können. Danach wird aus den Formeln abhängig von der gewählten Semantik ein Automat generiert, der dann für die RV genutzt werden kann.

Die Logik- und Automatenbibliothek RltlConv, die am ISP entwickelt wurde, beherrscht den vorher genannten Ablauf bereits für verschiedene Logiken, zum Beispiel für die Linear Temporal Logic (LTL) sowie drei- und vierwertige Semantiken dieser. Es fehlt aber eine Logik, mit der auch Echtzeiteigenschaften ausgedrückt werden können. Da es mit der Timed Linear Temporal Logic (siehe [1], dort EventClockTL genannt) möglich ist, solche Eigenschaften zu spezifizieren, ist eine Erweiterung von RltlConv um diese Logik sinnvoll. Wie LTL besitzt auch TLTL erstmal nur eine zweiwertige Semantik über unendlichen Worten. LTL wurde allerdings in [2] um eine vierwertige Semantik auf endlichen Worten (FLTL4) erweitert. Die Vorteile einer vierwertigen Semantik sind, dass die Semantik zwei endgültige Wahrheitswerte besitzt und außerdem auch noch Informationen über den aktuellen Stand der Auswertung geben kann.

In der BA soll eine vierwertige TLTL-Semantik analog zu der für LTL aus [2] und ein passendes Automatenmodell entwickelt werden. Außerdem soll die Umwandlung von Formeln für die Semantik in das passende Automatenmodell in RltlConv implementiert werden.

Ziele

•  Das Entwickeln einer vierwertigen TLTL-Semantik und passendem Automatenmodell.
•  Das Implementieren der Umwandlung in Scala.

Anforderungen

Es sollten die Grundlagen der Automatentheorie, wie zum Beispiel aus der Vorlesung "Theoretische Informatik", bekannt sein. Des Weiteren sollte die Motivation, Scala zu erlernen, vorhanden sein.

Literatur

[1] Thomas Henzinger, Jean-François Raskin und Pierre Yves Schobbens: Logics, Automata and Classical Theories for Deciding Real Time Languages
[2] Martin Leucker: Teaching Runtime Verification