Diplomarbeit am Lehrstuhl für Theorie der Programmierung, betreut durch Peter Massuthe und Prof. Wolfgang Reisig, eingereicht am 7. September 2005
Die Temporal Logic of Distributed Actions (TLDA) ist eine neue temporale Logik mit einer Halbordnungssemantik und eignet sich somit zur Spezifikation verteilter Systeme. Allerdings existieren für TLDA noch keine Werkzeuge, die die Spezifikation und Verifikation unterstützen. Die Verfügbarkeit solcher Werkzeuge trägt jedoch entscheidend zur Verbreitung der Logik bei.
In [Loh05] wurde mit der Ausarbeitung und Implementierung einer schrittbasierten Interleavingsemantik für TLDA die Grundlage für die Entwicklung eines expliziten TLDA-Modelcheckers gelegt. Der genaue Zusammenhang zwischen der Halbordnungs- und Interleavingsemantik wurde jedoch nicht bewiesen. Außerdem handelt es sich bei der Implementierung der Interleavingsemantik um einen Brute-Force-Prototyp, der nur für sehr einfache Spezifikationen in der Lage ist das Transitionssystem zu konstruieren.
Die formale Fundierung sowie die Ausarbeitung effizienter Algorithmen und Datenstrukturen ist Inhalt dieser Arbeit. Anhand mehrerer Fallstudien untersuchen wir die Leistungsfähigkeit des erweiterten Prototyps und illustrieren die Beziehung zwischen der Halbordnungs- und Interleavingsemantik.
Dateien
- Diplomarbeit (PDF-Dokument, 78 Seiten, 844 KB)
- Folien der Diplomverteidigung (PDF-Dokument, 37 Folien, 1882 KB)
letzte Kommentare