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 Algorithmen zum regulären Model-Checking

Ansprechpartner: Tim Strazny

Zusammenfassung

In dieser Arbeit geht es um den Nachweis der Korrektheit von Systemen mit beliebig vielen gleichartigen parallelen Komponenten. Der Nachweis soll unabhängig von der Anzahl der Komponenten sein. Dazu dient das reguläre Model-Checking, bei dem der Zustand eines Systems bestehend aus N gleichartigen Prozessen als Wort der Länge N aufgefasst und die möglichen Zustandsübergänge durch einen endlichen Automaten (dem Transducer) dargestellt wird. Das System ist parametrisch bezüglich der Anzahl der Prozesse und die Sprache der erreichbaren Zustände ist regulär. Zur Berechnung der Menge der erreichbaren Zustände wird der Transducer auf eine gewisse Weise verallgemeinert und auf die Menge der Anfangszustände angewandt. Das Model-Checking-Problem kann dann Schnitt-Leerheits-Problem für reguläre Sprachen aufgefasst werden: "Ist der Schnitt der Menge der erreichbaren Zustände und der Menge der schlechten Zustände leer?" Wobei die Menge der schlechten Zustände vom Benutzer festgelegt wird.

Für unsere Zwecke wählen wir die sogenannten Phasen-Event-Automaten (PEA) als Beschreibung des parametrisierten Systems. PEA sind kommunizierende Realzeitautomaten, die mit komplexen Daten umgehen können.

In einer vorangegangenen Arbeit wurde ein Algorithmus zur automatischen Erzeugung eines Transducers für PEA ohne komplexe Daten und ohne Zeit entwickelt und implementiert.

Ziel dieses individuellen Projekts ist es, die Menge der erreichbaren Zustände zu berechnen und damit das Model-Checking-Problem zu lösen. Desweiteren ist die Effektivität des implementierten Verfahrens an Fallbeispielen zu veranschaulichen. (In der Literatur werden Verfahren vorgestellt, mit denen die Menge der erreichbaren Zustände über den Transducer berechnet oder approximiert werden kann.)

In der Abteilung wurde eine höhere Spezifikationssprache entwickelt, die eine Kombination dreier Spezifikationssprachen für Kontrollfluss mit Kommunikationen, Datenoperationen und Zeit darstellt und deren Semantik durch PEA ausgedrückt wird. Im Programmwerkzeug Syspect ist eine automatische Übersetzung von CSP-OZ-DC-Schemata zu PEA integriert. Dieser Kontext öffnet u.a. folgende Möglichkeiten die Arbeit zu erweitern oder auszurichten:

• Festlegung schlechter Zustände auf höherer Ebene (CSP-OZ-DC)
• Integration in Syspect
• Regionen-/Zonen-Konstruktion für Daten (OZ-Teil)

Voraussetzungen:

• Kenntnis der Programmiersprache Java
• Erfolgreicher Abschluss der Veranstaltung Theoretische Informatik II (GTI)

Referenzen

1. Individuelles Projekt über die Berechung von Transducern aus PEA: Boris Rosenow. Reguläres Model-Checking für parametrisierte Phasen-Event-Automaten. 2010.
2. Übersichtsartikel zum regulären Model-Checking: Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Mayank Saksena. A Survey of Regular Model Checking. Proc. CONCUR'04. [ps]
3. Syspect-Webseite: http://csd.informatik.uni-oldenburg.de/~syspect/

1.2 Resource Management für KeYmaera

Ansprechpartner: Jan-David Quesel

Zusammenfassung

KeYmaera ist ein interaktiver Theorem-Beweiser zur Verifikation von hybriden Systemen basierend auf KeY. Theorem-Beweiser heisst, dass mithilfe eines Kalküls die Gültigkeit einer Formel gezeigt wird. Um dies zu tun wird die ursprüngliche Formel umgewandelt bis man schliesslich bei einer Formel ankommt für die ein anderes Tool uns sagen kann, ob diese wahr oder falsch ist.

Genau hier soll diese Arbeit ansetzen. Wir haben eine Reihe solcher Tools angebunden und es ist vorher nicht unbedingt möglich zu sagen, welches der Tools am schnellsten zu einem Ergebniss kommt. Daher wäre es sch&ooml;n diese Tools parallelisiert zu starten. Da allerdings nur eine begrenzte Zahl von Rechner bzw. Lizenzen zur Verfügung steht kann dies nicht einfach Naiv geschehen.

Im Rahmen der Arbeit soll hierfür ein Framework entwickelt werden und Heuristiken getestet werden.

Voraussetzungen:

• Kenntnis der Programmiersprache Java
• Erfolgreicher Abschluss der Veranstaltung Theoretische Informatik I (Logik)

Referenzen

KeYmaera Webseite, http://www.symbolaris.com/info/KeYmaera.html

Jan-David Quesel, A Theorem Prover for Differential Dynamic Logic: Deductive Verification of Hybrid Systems, Diplomarbeit, 2007 [pdf]

KeY Webseite, www.key-project.org

 

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:

• Algorithmen zum regulären Model-Checking
• Resource Management für KeYmaera

 

3 Abgeschlossene Studienarbeiten und Individuelle Projekte (Auswahl)

Implementierung eines Diagrammeditors für Shape-Diagramme in Eclipse

Sören Dierkes   (April 2012)

Implementierung einer Übersetzung der strukturellen Logik PSTL auf Pi-Kalkül-Prozessen in LTL auf Petrinetzen [pdf]

Sören Jeserich   (September 2011)

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)

 

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