Individuelle Projekte, Studien- und Diplomarbeiten

 

1 Ausgeschriebene Individuelle Projekte

Jede(r) Studierende muss nach der neuen Prüfungsordnung für BSc und Diplom ein individuelles Projekt durchführen (s. auch Leitfaden für Individuelle Projekte). Dieses ist selbstverständlich auch in unserer Abteilung möglich.

Erste Themenvorschläge finden Sie auf dieser Seite. Bei Fragen wenden Sie sich bitte an die genannten Ansprechpartner (auch unverbindlich). Weitere Themen können in persönlicher Absprache mit den Lehrenden der Abteilung vereinbart werden.

 

1.1 Weiterentwicklung des Werkzeugs Syspect

Ansprechpartner: Johannes Faber

Zusammenfassung

Syspect ist ein UML-Werkzeug, das die Entwicklung von Realzeitsystemen durch die graphische Modellierung von Komponenten-, Klassen- und Zustandsdiagrammen ermöglicht. Mit Hilfe von Syspect lassen sich Systeme entwickeln, für die insbesondere Kommunikationsaspekte, komplexe Datentypen und Realzeitverhalten zu berücksichtigen sind. Syspect wurde von einer Projektgruppe entwickelt und wird momentan im Rahmen des überregionalen Forschungsprojektes AVACS [3] eingesetzt. Das Werkzeug Syspect und weitere Informationen dazu sind auf der Syspect-Homepage [1,2] zu finden.

Im Umfeld von Syspect bieten sich verschiedene Ansatzpunkte sowohl für Individuelle Projekte/Bachelorarbeiten als auch für Diplomarbeiten/Masterarbeiten. Dies könnten zum Beispiel die folgenden Arbeiten sein:

• Entwicklung eines Type-Checkers für Syspect
  In Syspect werden Daten und Datenänderungen innerhalb von UML-Diagrammen mit der formalen Sprache Object-Z [5] spezifiziert. In der aktuellen Implementierung von Syspect werden die Object-Z-Ausdrücke auf korrekte Syntax überprüft. Allerdings wird nicht verifiziert, ob alle Datentypen zulässig verwendet werden. In diesem Projekt soll ein Type-Checker implementiert werden, der den Benutzer bei Bedarf über falsch verwendete Datentypen informiert.
• Entwicklung eines Verifikationsmanagers für Syspect
  In einer Diplomarbeit [4] ist bereits eine Anbindung von Syspect an einen Model-Checker sowie ein Simulator realisiert worden, mit deren Hilfe verifiziert werden kann, ob ein System, das mit Syspect entwickelt wurde, bestimmte gewünschte Eigenschaften (meist Sicherheitseigenschaften) erfüllt. Im Laufe der Entwicklung eines Systems werden oftmals eine Vielzahl von Eigenschaften überprüft. In diesem Projekt soll es darum gehen, Syspect um einen Verifikationsmanager zu erweitern, mit dessen Hilfe verschiedene Verifikationsläufe gesichert werden können. Dadurch soll insbesondere leicht ermöglicht werden, Benchmarks bei veränderten Rahmenbedingungen (zum Beispiel eine neue Version des Model-Checkers) zu wiederholen und zu vergleichen.
• Integration eines Editors für Phasen-Event-Automaten
  Ein Zwischenschritt bei der Anbindung von Model-Checkern an Syspect ist die Übersetzung eines Syspect-Models in Phasen-Event-Automaten (PEA). Zum besseren Verständnis von Systemen, zur Optimierung und zur Fehlerbehebung ist es oftmals sinnvoll sich die PEA-Darstellung anzusehen und sie bearbeiten zu können. Daher soll in diesem Projekt ein Editor für PEA in Syspect integriert werden, der dies ermöglicht. Darüber hinaus soll auch unterstützt werden, PEA direkt zu verifizieren. Ggf. kann auch ein Simulator [4] , der bereits für Syspect-Modelle existiert, genutzt werden, um sich mögliche Fehlerpfade direkt in den PEA anzeigen zu lassen.

Voraussetzungen: Da Syspect in Java implementiert ist, sollten Interessenten mit Java umgehen können. Darüber hinaus ist die Kenntnis der Syspect zugrundeliegenden Formalismen natürlich sehr nützlich aber nicht zwingend erforderlich.

An andere Interessen angepasste Themen und Aufgabenstellungen im Rahmen von Syspect sind eventuell möglich, daher sollten sich Interessenten an einen Mitarbeiter der Abteilung wenden. Beispielsweise könnte ein Projekt auch darin bestehen, eine größere Fallstudie mit Syspect zu untersuchen.

Referenzen

1. Syspect-Homepage, http://csd.informatik.uni-oldenburg.de/~syspect
2. Endbericht der Projektgruppe Syspect [pdf]
3. AVACS-Homepage, http://www.avacs.org
4. Diplomarbeit über die Model-Checker-Anbindung und den Simulator von Syspect:
   Ulrich Hobelmann, Verifying Properties of Processes, Data, and Time: Linking Counterexamples to High-Level Specifications, 2007
5. Graeme Smith, The Object Z Specification Language, Kluwer Academic Publishers, 2000

 

1.2 Entwicklung eines webbasierten Werkzeugs zur Unterstützung der Aufgaben als Herausgeber für die Zeitschrift „Acta Informatica“

Ansprechpartner: E.-R. Olderog

Zusammenfassung

Als Managing Editor der Zeitschrift Acta Informatica sucht Prof. Olderog ein System zur Dokumentenverwaltung. Die Aufgaben und Arbeitsvorgänge, die er und Andrea Göken hierbei zu bewältigen haben ähneln in gewissem Umfang denen, die bei der Ausrichtung einer Konferenz anfallen. Aus diesem Grund soll in diesem IP ein zu Konferenzsystemen ähnliches Werkzeug entwickelt werden, das webbasiert die Arbeitsvorgänge und Dokumentenverwaltung unterstützt.

Für die Konferenz FTRTFT, wurde als Konferenzsystem auf einem Server in der Abteilung die kostenlose, freie Version des START-Systems, START V1, eingesetzt und für die Konferenz angepasst. Das zu entwickelnde Werkzeug kann einen ähnlichen Ansatz verfolgen und ebenfalls auf das in Perl geschriebene START-System aufsetzen. Die Aufgabe kann aber auch in einer anderen Programmiersprache gelöst werden. Die System-Anforderungen, die das Werkzeug stellt, sollten aber vergleichbar sein.

Referenzen

1. Acta Informatica, http://link.springer.de/link/service/journals/00236/
2. FTRTFT, http://www.informatik.uni-oldenburg.de/ftrtft02/
3. START V1, http://www.softconf.com/START/startv1.html

1.3 JMoby/PLC: Portierung von Moby/PLC auf die Java Plattform

Ansprechpartner: Johannes Faber

Zusammenfassung

Ein Serie von Werkzeugen, die in der Abteilung Entwicklung korrekter Systeme entstanden sind, basieren auf der Moby Klassenbibliothek. Hierbei handelt es sich um eine in C++ geschriebene Klassenbibliothek, deren besonderer Fokus auf der Entwicklungung von Graph-Editoren liegt, die aber auch sehr plattformgebunden ist (Unix(-ähnliche) Systeme mit X11 Window System).

Um die Einsatzumgebungen für Moby zu erweitern wurde in der Diplomarbeit von Andreas Schulze [2] JMoby entwickelt. Bei JMoby handelt es sich um eine Java-Klassenbibliothek, deren Zielsetzung mit der von Moby vergleichbar ist, die aber wenn möglich auf Standard-Lösungen aus der Java-, bzw. JGraph-Bibliothek zurückgreift.

In diesem IP soll der Moby-Editor für SPS-Automaten, Moby/PLC, den man vielleicht auch schon aus der Vorlesung "Realzeitsysteme" oder dem Praktikum "Realzeitsysteme" kennt, mit JMoby umgesetzt werden.

Dieses IP kann auch als Diplomarbeit bearbeitet werden, wenn zusätlich die Simulation von SPS-Automaten (analog zum PLCSimulator) oder ein Export für Lego-Mindstorms entwickelt wird.

Referenzen

1. Moby-Webseite, http://csd.informatik.uni-oldenburg.de/~moby/
2. Andreas Schulze, Re-Design der MOBY-Klassenbibliothek in Java mit Implementierung eines graphischen Editors als Anwendungsbeispiel, Diplomarbeit, 2005 [pdf]
3. Moby/PLC, http://csd.informatik.uni-oldenburg.de/~moby/PLC/

 

2 Ausgeschriebene Diplomarbeiten

Diplomarbeiten werden individuell nach Absprache vergeben und betreut. Rechtzeitiges Informieren und Bekunden von Interesse sind von Vorteil. Wenden Sie sich an Prof. Olderog (zu den Sprechzeiten) oder gerne auch an seine Mitarbeiter(innen).

2.1 Weitere Themen für Diplomarbeiten

Durch ein Gespräch mit den Mitarbeitern können in der Regel auch aus eigenen Ideen Themen für Diplomarbeiten entwickelt werden. In vielen Fällen können auch Themen für Individuelle Projekte so erweitert werden, dass daraus eine Diplomarbeit wird.

Individuelle Projekte, die zu Diplomarbeiten erweitert werden können, sind unter anderem (aber nicht ausschließlich) die folgenden:

• Weiterentwicklung des Werkzeugs Syspect
• JMoby/PLC: Portierung von Moby/PLC auf die Java Plattform

 

3 Abgeschlossene Studienarbeiten und Individuelle Projekte (Auswahl)

XMI-Import und -Export für Syspect [pdf]

Dominik Denker   (Juli 2007)

Natürliches Schließen für den Shape Calculus [pdf]

Sven Linker   (April 2007)

MoDiShCa - Model Checking Discrete Shape Calculus [pdf]

Jan-David Quesel   (Sep. 2005)

Alternatives Backend für Jassda [pdf]

Johannes Rieken   (Juni 2005)

Entwicklung und Implementierung von Heuristiken zur optimierten Fehlersuche für PLC-Automaten [pdf]

Nico Mischok   (Mai 2005)

Anbindung einer Java-Implementierung an eine 3D-Animation [pdf]

Andreea Taifas   (Feb. 2005)

Entwicklung eines Javatools zur Übersetzung von Fehlerbäumen mit DC Semantik in Phasenautomaten [pdf]

Casjen Schnars   (Nov. 2004)

Temporallogische Spezifikation und CSP [ps]

Andreas Schäfer   (Okt. 2000)

Nicht-Implementierung von MIXGraphen unter PLGraph

Martin Friedrich   (Jun. 2000)

Fallstudie: Entwurf und Verifikation einer Zentralverriegelungssteuerung im KFZ mittels SPS-Automaten

Marc Lettrari   (Jul. 1999)

Z-Simulationstechniken als Grundlage für CSP-OZ-Simulation

Bernd Westphal   (Jun. 1999)

Ein Modelchecker für den Sequentiellen Duration Kalkül

Holger Rasch   (Mai 1999)

Untersuchung von HOL-Z anhand einer Fallstudie

Boris Wirtz   (Feb. 1999)

 

4 Abgeschlossene Diplomarbeiten (Auswahl)

Design By Contract for Java - Revised [pdf]

Johannes Rieken   (April 2007)

Verifying Properties of Processes, Data, and Time: Linking Counterexamples to High-Level Specifications

Ulrich Hobelmann   (April 2007)

A Theorem Prover for Differential Dynamic Logic: Deductive Verification of Hybrid Systems [pdf]

Jan David Quesel   (April 2007)

Integration von Verifikationswerkzeugen zur Systemanalyse mit Fehlerbäumen [pdf]

Casjen Schnars   (Oktober 2006)

Integration von CSP-OZ in die OO-Softwareentwicklung für die automatische Verifikation [pdf]

Andreea Stamer   (März 2006)

Runtime-Checking von JML-Spezifikationen mit Jass [pdf]

Martin Schnaidt   (Feb. 2006)

SAT-based Verification for Abstraction Refinement [pdf]

Stephanie Kemper   (Jan. 2006)

Model-Checking von Phasen-Event-Automaten bezüglich Duration Calculus Formeln mittels Testautomaten [ps.gz] [pdf]

Roland Meyer   (Aug. 2005)

Re-Design der MOBY-Klassenbibliothek in Java mit Implementierung eines graphischen Editors als Anwendungsbeispiel [pdf] [pdf]

Andreas Schulze   (Feb. 2005)

Fehlerbaumverifikation durch Modelchecking mit Uppaal [pdf]

Johannes Faber   (Mai 2004)

Trace- und Zeit-Zusicherungen beim Programmieren mit Vertrag [pdf]

Mark Brörkens   (Jan. 2002)

Verifikation von Beweiskizzen mit Hilfe von SPIN

Ingo Brückner   (Jan. 2002)

Fehlerbaumanalyse und Model-Checking [ps.gz]

Andreas Schäfer   (Dez. 2001)

Diskretes Model-Checking für SPS-Automaten

Tobe Toben   (Nov. 2001)

Eine Phasenautomatensemantik für SPS-Automaten

Henning Tschirner   (März 2001)

Sicherheitsanalyse eines Protokolls zur Vertragsunterzeichnung

Markus Wittwer   (März 2001)

Entwurf und Implementierung eines Algorithmus zur zeitlichen Analyse von Phasenautomaten

Holger Rasch   (Sep. 2000)

Übersetzung von Phasenautomaten in Timed Automata

Christian Mrugalla   (Jul. 2000)

Transforming CSP-OZ to Java assertions

Thies Wellpott   (Jun. 2000)

Trace Zusicherungen in Jass - Erweiterung des Konzepts ``Programmieren mit Vertrag''

Michael Plath   (Jun. 2000)

Eine Testautomatensemantik für Constraint Diagrams und ihre Anwendung

Marc Lettrari   (Apr. 2000)

Automatic conversion of the Formal Method CSP-OZ to FDR-CSP

Boris Wirtz   (Mär. 2000)

Parsing, Typchecking und Transformation von CSP-OZ nach Jass

Jens von Garrel   (Aug. 1999)

Hintergrundsimulation von SPS-Automaten [ps.gz]

Michael Möller   (Jul. 1999)

Graphische Spezifikationssprachen: Der Zusammenhang zwischen Constraint Diagrams und Real-Time Symbolic Timing Diagrams [ps.gz]

Jochen Hoenicke   (Jun. 1999)

Parallelität und Vererbung beim ``Programmieren mit Vertrag'' - Weiterentwicklung von JaWA -

Detlef Bartetzko   (Apr. 1999)

Implementierung von Constraint-Diagrammen

Marco Oetken   (Okt. 1998)

Implementierung und Optimierung eines Modelcheckers für Trace-Logik

Holger Bischoff   (Apr. 1998)

Graphische Spezifikationsformalismen

Volker Grabowski   (Dez. 1997)

Sequentieller Duration Kalkül

Arvid Hülsebus   (Okt. 1997)

``Programmieren mit Vertrag'' in Java

Dieter Meemken   (Sep. 1997)

Semantische Fundierung von CSP-Z

Stefan Hallerstede   (Jan. 1997)