|
|
 |
|
|
|
 |
|
|
|
| |
Musterbasierter Vergleich der Ausdrucksstärke temporaler Echtzeitlogiken
Zur Beschreibung dynamischer Eigenschaften eines Systems wurden verschiedene temporale Logiken (wie z.B. LTL oder CTL) entwickelt. Mit Hilfe dieser Logiken ist es z.B. möglich, Eigenschaften der folgenden Art zu spezifizieren: "Das System erreicht mit Sicherheit irgendwann einmal seinen Endzustand" oder "Die Bahnschranke kann nicht öffnen, bevor der Zug am Bahnübergang vorbeigefahren ist."
Diese Logiken spezifizieren Auftreten und Reihenfolge zwischen verschiedenen Ereignissen, sagen jedoch nichts über Zeitanforderungen, wie sie etwa in den folgenden Spezifikationen vorkommen: "Spätestens zehn Sekunden nachdem ein Rauchmelder Alarm meldet, wird automatisch die Feuerwehr informiert" oder "Wird der Knopf zweimal innerhalb einer Sekunde betätigt, wird das Licht angeschaltet." Für die Beschreibung solcher Zeitanforderungen existieren zahlreiche Formalismen. Dazu gehören Ableitungen der o.g. Logiken (etwa TCTL und TLTL) oder auch graphische Notationen.
Der erste Schritt der Diplomarbeit ist es, an Hand der Literatur eine Übersicht über die existierenden Formalismen zusammenzustellen. Hauptgegenstand der Arbeit ist dann ein bewertender Vergleich dieser Formalismen.
Dies soll an Hand eines Katalogs von am Lehrstuhl entwickelten Spezifikationsmustern (basierend auf den auf http://patterns.projects.cis.ksu.edu vorgestellten Mustern ohne Zeitanforderungen) geschehen. Insbesondere sollen die Spezifikationsmuster in den verschiedenen Formalismen dargestellt werden.
Das Thema der Diplomarbeit richtet sich an Studenten mit Interesse an formaler Logik und Automatentheorie. Bei Fragen oder Interesse wenden Sie bitte an Ralf Laue.
|
|
|
|
|
|
Über LPZ E-BUSINESS
Lehre
Lehrveranstaltungen
Abschlussarbeiten
Agile MDA
Series