Entwicklung korrekter Systeme

Ausgeschriebene Arbeiten

Jede(r) Studierende muss, je nach Studiengang, eine Bachelor- oder Masterarbeit schreiben. Das 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.

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).

Abgeschlossene Studienarbeiten und Individuelle Projekte (Auswahl)

  • Entwicklung eines Verification Managers für Syspect
    Jannis Stachowiak   (Juni 2010)

  • Reguläres Model-Checking für parametrisierte Phasen-Event-Automaten [pdf]
    Boris Rosenow   (März 2010)

  • Erweiterung von Syspect um einen Editor für Phasen-Event-Automaten [pdf]
    Matthias Peters   (Oktober 2009)

  • Werkzeuge für Bisimulationsäquivalenz von normierten Basic Parallel Processes
    Christian Kuka   (Mai 2008)

  • Graphische Benutzeroberfläche für HyKeY [pdf]
    Henning Rohlfs   (Februar 2008)

  • 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)

Abgeschlossene Diplomarbeiten (Auswahl)

  • Verifikationsarchitekturen in Syspect
    Matthias Peters   (August 2010)

  • Model checking pi-Calculus against temporal connectedness properties [pdf]
    Sven Linker   (Dezember 2008)

  • Entwurf und Implementierung von Algorithmen zur Berechnung von Petrinetz-Semantiken für Pi-Kalkül-Prozesse [pdf]
    Tim Strazny   (Juli 2007)

  • Design By Contract for Java - Revised [pdf]
    Johannes Rieken   (April 2007)

  • Verifying Properties of Processes, Data, and Time: Linking Counterexamples to High-Level Specifications [pdf]
    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)