Studien- und Diplomarbeiten

Offene Themen

Bereich Verifikation

Verteilte Algorithmen

Problemstellung	Anwendungen und Organisation rechnergestützter Systeme sind zunehmend verteilt. Damit werden verteilte Algorithmen immer wichtiger. In dieser Arbeit modellieren Sie einen verteilten Algorithmus aus der Literatur mit Petrinetzen, Temporaler Logik, Abstract State Machines, Z oder einer anderen Spezifikationstechnik, beweisen seine wichtigsten Eigenschaften und vergleichen die gewählte Technik mit Alternativen.
Ziele	- Modellierung eines verteilten Algorithmus mit einer Spezifikationstechnik - Beweis von Eigenschaften - Vergleich der gewählten Technik mit Alternativen
Voraussetzungen	Teilnahme an mindestens einer der Vorlesungen Methoden und Modelle des Systementwurfs bzw. Verteilte Algorithmen
Beginn	sofort
Ansprechpartner	Prof. Dr. Wolfgang Reisig

Komposition von Petrinetzen

Problemstellung	Große Systemmodelle werden systematisch durch Komposition kleinerer Modelle kkonstruiert. Für Petrinetz-Modelle braucht man deshalb geeignete Kompositions-Operationen. In der Literatur werden zahlreiche solche Operationen vorgestellt. Sie sind oft intuitiv einfach, aber formal doch vergleichsweise aufwendig.
Ziele	Vor dem Hintergrund ganz neuer Vorschläge werden in dieser Diplomarbeit bekannte Konstruktionen neu bewertet, neu formuliert und aufeinander bezogen. Neue Varianten werden systematisch hergeleitet und untersucht.
Voraussetzungen	Grundkenntnisse zu Petrinetzen, wie sie in den Vorlesungen "Methoden und Modelle des Systementwurfs" und "Verteilte Algorithmen" vermittelt werden. Dieses Thema erfordert Interesse an guten, einfach verständlichen und dennoch präzisen formalen Darstellungen.
Beginn	sofort
Ansprechpartner	Prof. Dr. Wolfgang Reisig
Umfang/Rahmen	eine Diplomarbeit

Offene Netze und Bedienungsanleitungen

Stochastische Bedienungsanleitungen

Problemstellung	Wenn bisher stochastische Petrinetze betrachtet wurden, dann im Zusammenhang mit geschlossenen Systemen, d.h. es fand keine Kommunikation mit der Umgebung oder genauer mit einem Partnernetz statt. Am Lehrstuhl betrachten wir jedoch kommunizierende Systeme in Form von offenen Netzen, also Petrinetzen die Kommunikationsplätze besitzen können. Um zu beschreiben, wie ein möglicher Partner P eines gegebenen Netzes N ausschauen darf, wurde am Lehrstuhl das Konzept der Bedienungsanleitungen entwickelt. Im Zusammenhang mit stochastischen Netzen stellen sich hier zwei Fragen: 1. Wenn ein Partner P in einem bestimmten Zustand, mit welcher Wahrscheinlichkeit ist N in welchem Zustand? 2. Analog dazu, was lässt sich über die Zustände von P sagen, wenn N in einem bestimmten Zustand ist.
Ziele	Es soll der Formalismus der Stochastischen Petrinetze auf offene Netze erweitert werden. Auf Basis der dafür notwendigen Definitionen soll der Begriff der Bedienungsanleitung um stochastische Informationen erweitert werden, mit dem Ziel, die beiden zuvor genannten Fragen beantworten zu können. Die Ergebnisse sollen anschließend in die am Lehrstuhl existierende Toollandschaft integriert werden.
Voraussetzungen	Sehr empfohlen sind stochastische Grundkenntnisse und Erfahrung in C++, wünschenswert sind Kenntnisse über Petrinetze.
Ansprechpartner	Christian Gierds
Umfang/Rahmen	eine Diplomarbeit

Laufende Arbeiten

Diplomarbeiten

Studienarbeiten

Implementierung einer grafischen Benutzeroberfläche für Tools4BPEL (Janine Ott)

Problemstellung	Am Lehrstuhl werden seit Oktober 2005 im Projekt Tools4BPEL mehrere Werkzeuge zur Analyse von Geschäftsprozessen entwickelt. Diese Prototypen werden derzeit mit Kommandozeilenparametern kontrolliert, was ob der Fülle an Funktionen zunehmend unübersichtlich wird. Damit auch Nicht-Experten die Werkzeuge benutzen können, soll eine grafische Benutzeroberfläche (GUI) implementiert werden, die die Funktionen der einzelnen Werkzeuge übersichtlich darstellt und (bswp. mit Hilfe von Assistenten) oft verwendete Anwendungsszenarien unterstützt.
Ziele	Da die Werkzeuge in C++ geschrieben sind, soll auch die GUI in dieser Sprache implementiert werden. Um weiterhin Plattformunabhängigkeit (Windows, Linux, Mac OS) sicherzustellen, bietet sich die Qt-Bibliothek von Trolltech http://trolltech.com/products/qt an. Die GUI soll die bestehenden Werkzeuge ausreichend einfach steuern und den Nutzer weitgehend unterstützen. Weiterhin soll die GUI leicht für neue Funktionen erweiterbar sein. Zuletzt sollen grundlegende Funktionen implementiert werden, mit denen von den Werkzeugen erstellte Dateien (z.B. XML-Dokumente oder PNG-Grafiken) innerhalb der GUI angezeigt werden können.
Voraussetzungen	Kenntnisse in der Programmiersprache C++ sind vorteilhaft. Kenntnisse der Qt-Bibliothek sind hilfreich, jedoch wegen einer exzellenten Dokumentation nicht notwendig.
Ansprechpartner	Christian Gierds
Umfang/Rahmen	eine Studienarbeit

Stochastische Petrinetze in Toollandschaft integrieren (Thomas Kuhlmeyer)

Problemstellung	Am Lehrstuhl existieren verschiedene Tools, welche auf einem Erreichbarkeitsgraphen eines Petrinetzes arbeiten. Dafür haben sich mittlerweile Datenformate etabliert. Außen vor gelassen wurden dabei bisher stochastische Annotationen an den Petrinetztransitionen. Es gibt bereits Werkzeuge, die für ein stochastisch annotiertes Petrinetz den Erreichbarkeitsgraphen bestimmen können, sodass für jeden Knoten die Wahrscheinlichkeit gegeben ist, in diesen zu gelangen. Hier fehlt jedoch die Anbindung an unsere Tools.
Ziele	Unsere Toollandschaft soll möglichst einfach und effizient auf stochastische Informationen zugreifen können. Dazu sollen - die existierenden Tools für die Analyse Stochastischer Petrinetze evaluiert werden, und ein geeignetes gewählt werden, - die Ausgabe des gewählten Tools unseren Tools zur Verfügung gestellt werden, sowie - die vorhandenen Datenformate angepasst werden.
Voraussetzungen	Sehr empfohlen sind stochastische Grundkenntnisse und Erfahrung in C++, wünschenswert sind Kenntnisse über Petrinetze.
Ansprechpartner	Christian Gierds
Umfang/Rahmen	eine Studienarbeit

Auswertung von Mutex-Algorithmen (Antoniya Georgieva)

Problemstellung	Das Problem des wechselseitigen Ausschlusses (Mutex) wurde 1965 von E. Dijkstra definiert und gelöst. Seitdem wurden zahlreiche Algorithmen vorgestellt, die der Prozess-Synchronisation dienen und von zentraler Bedeutung für nebenläufige Systeme sind. Aufgabe dieser Verfahren ist, den Zugriff auf gemeinsam genutzte Daten so zu gestalten, dass Prozesse/ Clients diese koordiniert lesen und verändern und somit der konsistente Zustand des Systems zu jedem Zeitpunkt erhalten bleibt.
Ziele	Im Rahmen dieser Arbeit soll eine Auswahl an bewährten Verfahren vorgestellt werden, die das Mutex-Problem lösen. Ziel ist, diese zu vergleichen und neben ihre Vor- und Nachteile, die getroffenen Annahmen aufzuzeigen, unter denen die gewählten Ansätze die gestellten Anforderungen erfüllen.
Ansprechpartner	Prof. Dr. Wolfgang Reisig
Umfang/Rahmen	eine Studienarbeit