Visualisierung von LTL-Gegenbeispielen (in Java/Eclipse)

Das Thema ist bereits vergeben!

LTL (Linear Temporal Logic) wird dazu verwendet, zeitabhängige Eigenschaften von Systemen auszudrücken. Zum Beispiel Aussagen wie "Springt die Ampel auf Gelb, wird sie in Zukunft auf Rot springen und bis dahin gelb bleiben." Der am Lehrstuhl entwickelte Model-Checker ProB unterstützt auch das Prüfen solcher Formeln. Wenn ein System die Formeln nicht erfüllt, wird dem Benutzer ein Gegenbeispiel angezeigt.

Ein Problem (und Thema der Arbeit) ist, dass solche Gegenbeispiele nicht immer leicht zu verstehen sind. Zu entwickeln wäre ein Werkzeug, das dem Benutzer zeigt, warum ein Pfad (eine Abfolge von Systemzuständen und Ereignissen) ein Gegenbeispiel ist und warum Teile der Formel in einem bestimmten Zustand gerade wahr oder falsch sind.

Die zu entwickelnde Software wäre ein mittels Java entwickeltes Eclipse-Plugin. Voraussetzung wären gute Java-Kenntnisse, keine Angst vor ein bisschen Logik und Interesse daran, wie etwas Benutzern verständlich präsentiert werden könnte.

Bachelor- / Master- oder Projektarbeiten je nach Absprache.