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
TLDC berechnet die Aktionen einer TLDA-Spezifikation und konstruiert den Erreichbarkeitsgraphen.
Links
Studienarbeit am Lehrstuhl für Theorie der Programmierung (20. Juni 2005)
Die Temporal Logic of Distributed Actions (TLDA) ist eine temporale Logik mit einer Halbordnungssemantik und eignet sich somit zur Spezifikation verteilter Systeme. Allerdings gibt es noch wenig Erfahrung bei der computergestützten Verifikation halbordnungsbasierter Formalismen. Viele bekannte effiziente Algorithmen des expliziten Modelchecking setzen ein Transitionssystem und somit eine Interleavingsemantik voraus.
In dieser Arbeit wird eine Interleavingsemantik für TLDA vorgeschlagen und ein Prototyp entwickelt, der für eine bestimmte Klasse von TLDA-Spezifikationen das Transitionssystem aufbaut. Die entwickelte Semantik soll zusammen mit dem Prototypen die Grundlage für die weitere Arbeit an einem Modelchecker für TLDA sein.
Dateien
Vortrag beim Workshop “Luhme XI” beim Lehrstuhl für Theorie der Programmierung (7. Mai 2005)
Dieser Vortrag gibt die voraussichtliche Gliederung meiner Studienarbeit wieder: nach einer kurzen Einführung in TLDA vergleichen wir verschiedene Semantiken (Halbordnung vs. Interleaving) miteinander, arbeiten formal ein Transitionssystem für TLDA-Spezifikationen aus und zeigen an Beispielen, wie dies prototypisch im Tool TLDC implementiert wurde. Außerdem werden Lösungen für auftretende (zumeist exponentielle) Probleme vorgestellt.
Dateien
Zusammenfassung der Vorlesung DBS I – Grundlagen von Datenbanksystemen (Wintersemester 2004/2005) bei Prof. Johann Christoph Freytag zur Klausurvorbereitung, sowie Praktikumaufgaben mit Lösungen
In der Zusammenfassung werden die Themen Architektur und Eigenschaften von Datenbanksystemen, Entity-Relationship-Modell, Relationenmodell, Entwurf relationaler Datenbanken, Relationale Anfragesprachen, Anfragebearbeitung in relationalen Datenbanksystemen und Speicherstrukturen für Datenbanken beschrieben.
Themen der Praktikumaufgaben sind Modellierung zu Entity-Relationship-Modellen, Transformation ERM nach RM, Schlüsselkandidaten, Normalformen, Normalisierung, SQL (Abfragen, Trigger, Constraints) und JDBC.
Dateien
letzte Kommentare