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

Laufende Arbeiten

Diplomarbeiten

Laufzeitumgebung für adaptive Prozesse (Manja Wolf)

Problemstellung	Für bestimmte Prozessbeschreibungen, wie z. B. im Katastrophen- oder Krisenmanagement, ist es wünschenswert oder sogar erforderlich, die Prozessbeschreibung während der Laufzeit des Prozesses zu verändern. Durch die Veränderungen des Originalprozesses können Handlungsoptionen (und damit Pfade im Zustandsraum) unmöglich werden oder auch neue Optionen entstehen. Um derartige Prozessdynamik formal zu beschreiben, wurden "adaptive Prozesse" auf der Basis von Petrinetzen definiert. Der Hauptprozess (das Petrinetz) wird um annotierte Netz"schnipsel" (Oclets) mit Vorbedingungen erweitert. Oclets beschreiben vom Originalprozess abweichendes, alternatives Verhalten und werden nach Eintreten der Vorbedingungen in das Originalnetz eingefügt oder entfernt (Anti-Oclets). Sie verändern den ursprünglichen Prozess, erweitern ihn oder/und inaktivieren bzw. entfernen möglicherweise Pfade im Zustandsraum. Ob das von einem Oclet beschriebene Verhalten keinesfalls eingebaut werden darf, eingebaut werden muss oder darf, wird mit Konzepten der Live Sequence Charts ausgedrückt. Hierfür werden einzelne Knoten des Netzes mit Temperaturen annotiert und das gesamte Oclet typisiert. Für diese adaptiven Prozesse existiert derzeit keine Laufzeitumgebung, mit der der theoretische Ansatz überprüft werden kann.
Ziele	Im Rahmen der Diplomarbeit wird eine Laufzeitumgebung zur Definition und Simulation von adaptiven Prozessen erstellt. Grundlage der Programmierung sind die Eclipseprojekte EMF (Eclipse Modeling Framework), GEF (Graphical Editing Framework) und GMF (Graphical Modeling Framework). Es soll möglich sein, - Adaptive Prozesse, also einen Hauptprozess und n Oclets zu definieren und Knoten je nach "Temperatur" zu färben; - den Hauptprozess ablaufen (schalten und in einen Endzustand gelangen) zu lassen; - Oclets auf den Hauptprozess anzuwenden (Knoten einfügen/entfernen) und den Hauptprozess hierdurch zu verändern. Von der Laufzeitumgebung soll entschieden werden, ob die Vorbedingungen erfüllt sind, das Oclet angewendet werden darf/muss/nicht darf, was nach dem Anwenden des Oclets mit nachfolgenden Knoten bzw. parallelen/alternativen Knoten im Hauptprozess geschieht. Ob das Einbauen eines Oclets weitere Oclets erfordert (z.B. Anti-Oclets, die Teile aus dem Originalnetz löschen); - neue Oclets zur Laufzeit eines Prozesses zu definieren bzw. bestehende Oclets zu verändern. Die Laufzeitumgebung soll entscheiden, ob die veränderten/neuen Oclets erlaubt, d.h. zum Hauptprozess kompatibel sind; - die entstehenden Netze zu exportieren, um sie mit den am Lehrstuhl vorhandenen Tools zu analysieren.
Publikationen	Dirk Fahland: A Formal Approach to Adaptive Processes using Scenario-based Concepts.
Betreuer	Dirk Fahland
Umfang/Rahmen	eine Diplomarbeit

Statische Analyse von BPEL (Thomas Heidinger)

Problemstellung	Bei der statischen Analyse werden Eigenschaften bereits am Quelltext eines Programms untersucht. Die jetzige Analyse von BPEL abstrahiert von Datenaspekten, wodurch das zugrundeliegende Modell einfacher wird. Da Daten jedoch den Kontrollfluss maßgeblich beeinflussen, wird die Analyse auch unpräziser.
Ziele	- Anwendung statischer Analyse auf BPEL. - Einbeziehung von Daten zur Verbesserung der Analyse
Publikationen	Thomas Heidinger: Statische Analyse von BPEL4WS-Prozessmodellen
Betreuer	Niels Lohmann
Umfang/Rahmen	eine Diplomarbeit

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.
Beginn	sofort
Ansprechpartner	Christian Gierds
Umfang/Rahmen	eine Studienarbeit

Neue Reduktionstechniken (Robert Prüfer)

Problemstellung	Bei der Suche nach erreichbaren Zuständen in Transitionssystemen kann mittels der Sweep-Line-Methode Speicherplatz gespart werden, indem einmal gefundene und nicht mehr benötigte Zustände gelöscht werden. Dafür wird eine Progress Measure benötigt, um zu entscheiden, welche Zustände gelöscht werden können. Für Petrinetze kann diese Progress Measure automatisch berechnet werden; allerdings lässt die bisherige Berechnung verschiedene Freiheitsgrade zu. Unter Anwendung verschiedener heuristischer Optimierungsverfahren soll untersucht werden, ob die Progress Measure verbessert werden kann.
Ziele	Finden geeigneter Heuristiken zur Steigerung der Leistungsfähigkeit der Sweep-Line-Methode
Ansprechpartner	Christian Stahl, Daniela Weinberg
Umfang/Rahmen	eine Studienarbeit

Modellierung kommunizierender Systeme (Mike Herzog)

Problemstellung	Am Lehrstuhl wurden Algorithmen zur Analyse kommunizierender Services entwickelt und implementiert. In dieser Studienarbeit sollen als Fallstudie mehrere kommunizierende Systeme (z.B. Kommunikationsprotokolle wie SMTP, HTTP, SOAP, etc.) in ein Petrinetzmodell überführt und mit den bestehenden Werkzeugen analysiert werden.
Ziele	- Modellieren von Kommunikationsprotokollen mit Petrinetzen
Ansprechpartner	Daniela Weinberg
Umfang/Rahmen	eine Studienarbeit

Übersetzung von UML2 Aktivitätsdiagrammen in OWFNs (Martin Znamirowski)

Problemstellung/Ziel	Es soll ein Algorithmus erarbeitet werden, welcher BOM-Geschäftsprozess-Modelle des IBM Websphere Business Modeler unter Bewahrung des Verhaltens in die Petrinetz-Klasse der offenen Workflow-Netze (oWFN) übersetzt. Weiterhin soll eine Methode gefunden werden, ein generiertes oWFN anhand der Rollenzuweisungen der verschiedenen Prozessaktivitäten aufzutrennen. Das Ergebnis dieser Dekomposition sollen rollenbezogenen Komponenten sein, die jeweils die Aktivitäten der entsprechende Rolle und das Prozessverhalten bezüglich dieser Aktivitäten enthalten. Dabei soll jede Komponente über eine geeignete Schnittstelle zu den anderen Komponenten verfügen, so dass ihre Komposition entlang der Schnittstelle das Verhalten des ursprünglichen Prozesses ergibt. In dieser Sicht bildet jede Komponente die geeignete Basis für eine Service-orientierte Implementation des Gesamtprozesses. Im Ergebnis der Arbeit soll ein Werkzeug entstehen, die die vom IBM Websphere Business Modeler erzeugte XML-seralisierte Darstellung eines BOM in oWFN Notation übersetzt und die Dekompositionsoperation implementiert.
Betreuer	Dirk Fahland
Umfang/Rahmen	eine Studienarbeit

Modellierung des Workflows der Taskforce Erdbeben des GFZ mit Petrinetzen (Konstanze Swist)

Problemstellung	Die Task Force Erdbeben am GFZ Potsdam erforscht - teilweise auch vor Ort - geophysikalische Prozesse, die während und nach Katastrophenbeben ablaufen. Die Vorgehensweise dabei soll modelliert werden. Es existiert bereits ein Prozessmodell in einfacher Flussdiagramm-Notation, welches den planmäßigen Ablauf darstellt, sowie ein in derselben Notation verfasstes Ablaufmodell auf Grundlage von Vorgangsprotokollen eines tatsächlichen Einsatzes.
Ziele	Ziel ist die Beschreibung des Prozessmodells in einer Eingabesprache für Petrinetzwerkzeuge. Dafür muss zuvor das Prozessmodell an die tatsächlichen Gegebenheiten aus dem Ablaufmodell angepasst werden.
Betreuer	Dirk Fahland
Umfang/Rahmen	eine Studienarbeit