Aktuelle Studien-, Diplom-, Bachelor- und Masterarbeiten

Title Betreuer Status
Untersuchung und Entwicklung eines Lokationssystems Markus Maron zu vergeben

Untersuchung und Entwicklung eines Lokationssystems


Kategorie: Diplom-, Master-, Studien-, Bachelorarbeit

Keywords: Bluetooth, Mobile Phone, Networks, triangulation

Es gibt verschiedene Methoden, die zur Bestimmung der Postion eines Benutzers verwendet werden können. Bekannte Techniken sind z.B. via GPS, WLAN, Bluetooth, Cell-ID, unter Berücksichtigung der relativen Nähe, Signalstärke oder mit Triangulation. Diese gilt es zu untersuchen und zu implementieren.

Kontakt: Markus Maron (B215, maron@uni-koblenz.de ).


Arbeiten die abgeschlossen oder in Bearbeitung sind


Title Betreuer Status
Pedestrian Navigator Markus Maron Ildar Klasen (In Bearbeitung)
Display Steuerung durch Personen Erkennung Markus Maron Daniel Künster (In Bearbeitung)
Recommender System für Campus News/Stadtinfo Markus Maron Christoph Ehrsfeld (In Bearbeitung)
Campus News: Entwicklung eines ambienten Social-Networks Markus Maron Marius Rackwitz (In Bearbeitung)
Erweiterung von LogAnswer durch profilbasierte Antwortauswahl Björn Pelzer Timo Eifler (In Bearbeitung)
Erweiterung des E-hyper tableau Kalkuels und dessen Implementierung in den Beweiser EKRHyper Björn Pelzer Markus Bender (In Bearbeitung)
Entwicklung einer grafischen Benutzerschnittstelle für den Theorembeweiser E-KRHyper Björn Pelzer Heiko Richter (abgeschlossen)
Automatische Analyse logischer Probleme Björn Pelzer Timo Eifler (abgeschlossen)
Präkompilation von TPTP-Problemen mit komplexen Hintergrundtheorien Björn Pelzer Heiko Günther (abgeschlossen)
fnnlib - A Flexible C++ Library for Recurrent Neural Network Simulations Björn Pelzer Dennis Fassbender (abgeschlossen)
Creating an Abstract Physics Layer for Simspark Björn Pelzer Andreas Held (abgeschlossen)
Ambientes Digital Right Management am Beispiel elektronischer Fahrscheine Sebastian Magnus Heiko Richter
(abgeschlossen)
Sichere und effiziente Ende-zu-Ende Übertragung in hybriden Bluetooth - WLAN Netzen Markus Maron Christoph Ersfeld
(abgeschlossen)
Testen von Verifikations-Werkzeugen Thorsten Bormer Markus Wagner
(abgeschlossen)
Verifikation von Algorithmen-Implementationen Bernhard Beckert Volker Klasen
(abgeschlossen)
Using formal specifications for Common Criteria Certification Bernhard Beckert Sarah Grebing (abgeschlossen)

Pedestrian Navigator


Kategorie: Diplomarbeit

Keywords: Mobile Phone, navigation

Ziel ist es ein Navigationssystem für das iPhone zu entwickeln, das speziell auf Fußgänger ausgerichtet ist und mit einem individuellen Profil arbeitet.

Kontakt: Markus Maron (B215, maron@uni-koblenz.de ).


Display Steuerung durch Personen Erkennung.


Kategorie: Bachelorarbeit

Keywords: gesture recognition

Ein Display soll durch die Wiedererkennung einer Person gesteuert werden. Dazu sollen verschiedene Methoden zur Umsetzung erforscht und umgesetzt werden.

Kontakt: Markus Maron (B215, maron@uni-koblenz.de ).


Recommender System für Campus News/Stadtinfo


Kategorie: Masterarbeit

Keywords: Mobile Phone, Navigation, point of interest recommendation

Es soll ein System entwickelt werden, dass auf Basis der Aktivität eines Benutzers Empfehlungen für Sehenswürdigkeiten, Nachrichten/Kategorien oder Touren aus- spricht.

Kontakt: Markus Maron (B215, maron@uni-koblenz.de ).


Campus News: Entwicklung eines ambienten Social-Networks


Kategorie: Baechelorarbeit

Keywords: Bluetooth, Security, Mobile Phone, Networks

Campus News ist ein Service-Angebot der Universität Koblenz-Landau und des Studierendenwerks Koblenz. Aktuelle Informationen werden per Bluetooth auf die Handys oder PDAs von Studierenden und Mitarbeitern übertragen und in Kurzform auf den multimedialen Displays in den Mensen dargestellt.

Jetzt habt ihr die Gelegenheit, aktiv bei der Erweiterung von Campus News mitzuwirken:

  • Schickt Nachrichten von eurem Handy völlig kostenfrei im Campus News Netz direkt an eure Freunde via Bluetooth, oder
  • Teilt euren Kommilitonen über die Beamerfläche mit, was ihr zu sagen habt (Twitter) oder
  • Erweitert das Benutzerportal um einen Instant Messenger und integriert einen Buddylocator.

Kontakt: Markus Maron (B215, maron@uni-koblenz.de ).


Erweiterung von LogAnswer durch profilbasierte Antwortauswahl


Kategorie: Diplomarbeit

Keywords: Natural Language Processing, Semantic Desktop, Profile Information

LogAnswer ist ein auf logischen Inferenzverfahren basierendes System zur inhaltlichen Beantwortung natürlichsprachlicher Fragen an große textuell gegebene Wissensbestände. Zur Beantwortung der Fragen werden, auf Basis von unterschiedlichen Kriterien, relevante Textstellen aus dem Hintergrundwissen extrahiert.

Im Rahmen dieser Arbeit soll untersucht werden ob eine Übereinstimmung mit Benutzer bezogenen Profildaten als zusätzliches Kriterium für dieses Auswahlverfahren sinnvoll genutzt werden kann. Als Quelle für die Profildaten wird dabei exemplarisch das Semantic Desktop System NEPOMUK verwendet.

Kontakt: Timo Eifler.

Betreuer: Björn Pelzer


Erweiterung des E-hypertableau-Kalküls und dessen Implementierung in den Beweiser E-KRHyper


Kategorie: Diplomarbeit

Keywords: Theorembeweiser, E-KRhyper, E-hypertableau, unique name assumption, nichtmonotones Schließen

E-KRHyper ist ein automatischer Theorembeweiser. Er ist eine Implementierung des E-hypertableau-Kalküls, der die Vorzüge von analytischen Tableaux und hyper resolution verbindet.

Ziel der Diplomarbeit ist es, sowohl den Kalkül als auch dessen Implementierung in zwei Punkten zu erweitern. Zum einen soll die Möglichkeit des nichtmonotonen Schließens ausgebaut werden und zum anderen soll die Behandlung der unique name assumption eingeführt werden.

Kontakt: Markus Bender.

Betreuer: Björn Pelzer


Entwicklung einer grafischen Benutzerschnittstelle für den Theorembeweiser E-KRHyper


Kategorie: Diplom- oder Masterarbeit

Keywords: Deduktion, Logik, GUI-Programmierung

E-KRHyper ist ein automatischer Theorembeweiser, entwickelt an der Universität Koblenz. Er liest logische Probleme in Prolog-ähnlicher Darstellung ein und berechnet dazu Modelle oder Widerspruchsbeweise. Zur Zeit arbeitet E-KRHyper ausschließlich kommandozeilenbasiert. Die Aufgabenstellung der Diplomarbeit ist die Entwicklung einer grafischen Benutzeroberfläche (GUI) für den Theorembeweiser, vergleichbar mit der des Beweisers Prover9, siehe: http://www.cs.unm.edu/~mccune/mace4/gui/v05.html

Im Einzelnen:

  • Laden und Speichern von logischen Problemdateien,
  • Ansteuern des Beweisvorgangs (Start, Abbruch, Kontrollparameter, etc.)
  • grafische Darstellung der Beweisergebnisse.

Voraussetzungen:

  • Programmierkenntnisse (E-KRHyper ist in OCaml geschrieben, aber für die GUI sind auch andere Sprachen möglich), Prologkenntnisse sind hilfreich,
  • Logikkenntnisse (Prädikatenlogik, Tableaukalkül),
  • Einarbeitung in die Bedienung von E-KRHyper (kann während der Diplomarbeit geschehen),
  • Einarbeitung in den Quellcode des Beweisers ist nicht unbedingt nötig.

Kontakt: Björn Pelzer (B225, bpelzer@uni-koblenz.de, http://www.uni-koblenz.de/~bpelzer/ekrhyper ).


Automatische Analyse logischer Probleme


Kategorie: Diplom- oder Masterarbeit

Keywords: Deduktion, Logik

Der hier an der Universität Koblenz entwickelte automatische Theorembeweiser E-KRHyper verarbeitet logische Probleme in Prolog-ähnlicher Syntax. Die dabei verwendete Beweisstrategie kann durch eine Reihe von Parametern beeinflusst werden. Momentan müssen diese Parameter von Hand an das jeweilige Problem angepasst werden, weswegen bei umfangreicheren Testserien über viele Probleme hinweg nur Standardparameter benutzt werden, die im Einzelfall aber sehr ungünstig sein können. Die Aufgabenstellung der Diplomarbeit ist die Entwicklung eines Präprozessors, der logische Probleme analysiert und anhand ihrer Merkmale automatisch individuelle Parameter festlegt.

Die Aufgabenstellung ist vergleichsweise frei: Man kann im Rahmen der Prädikatenlogik kreativ werden und wird viel ausprobieren müssen, was funktioniert und was nicht. Das Resultat wird als integraler Bestandteil von E-KRHyper in Anwendungen zum Einsatz kommen.

Voraussetzungen – das meiste kann auch während der Diplomarbeit erlernt werden:

  • Programmierkenntnisse (E-KRHyper ist in OCaml geschrieben, und für eine eventuelle Integration des Präprozessors sollte auch hierfür Ocaml verwendet werden),
  • Logikkenntnisse (Prädikatenlogik, Tableaukalkül),
  • Einarbeitung in die Bedienung und in kleine Teile des Quellcodes von E-KRHyper.

Kontakt: Björn Pelzer (B225, bpelzer@uni-koblenz.de, http://www.uni-koblenz.de/~bpelzer/ekrhyper ).


Ambientes Digital Right Management am Beispiel elektronischer Fahrscheine


Kategorie: Studienarbeit

Keywords: Ambient Systems, Digital Right management, Authenticity, Electronic Ticketing

Bearbeitet von: Heiko Richter

Fahrkarten, Eintrittskarten, Schlüssel und Berechtigungen zu Dienstleistungen werden vermehrt in elektronischer Form angeboten: Ob als Chipkarte, elektronisches Zahlenschloss, RFID-Tag oder Funkeinheit im Autoschlüssel. Sie haben gemeinsam, dass sie einen beschränkten Nutzerkreis zu einem Dienst berechtigen, von dem andere ausgeschlossen sind.

Menschen erkennen eine Person am Aussehen und können ein Gesicht mit einem Lichtbild vergleichen. Wie aber werden Erlaubnisse elektronisch geprüft?

Die Studienarbeit soll digitale Rechteverwaltung am Beispiel elektronischer Fahrkarten untersuchen. Dabei stehen Fragen im Vordergrund, wie ein Nutzer nachweisbar erkannt wird, wie seine Rechte in einer mobilen, dynamischen Umgebung erkannt werden, wie diese vor Missbrauch (Fälschung, Weitergabe) geschützt werden und welche Medien als Träger geeignet sind. Die Ergebnisse werden in einer Java Implementation nachgewiesen.

Kontakt: Sebastian Magnus (B 225, smagnus@uni-koblenz.de).


Sichere und effiziente Ende-zu-Ende Übertragung in hybriden Bluetooth - WLAN Netzen


Kategorie: Bachelorarbeit

Keywords: Networks, Protocols, Heterogenous Systems

Bearbeitet von: Christoph Ersfeld

 

Kopfhörer, Autoschlüssel, Mobiltelefone: Ob zum Austausch von Visitenkarten, als Freisprecheinrichtung während der Autofahrt oder als Ersatz für herkömmliche Kabel, Bluetooth wird immer stärker in unseren Alltag integriert.

Die Bluetooth-Spezifikation berücksichtigt Sicherheit auf Punkt-zu-Punkt Ebene, beachtet aber nur eine Auswahl von in der Praxis relevanten Aspekten. Ende-zu-Ende Verbindungen bleiben zunächste ungeschützt: Korrupte Zwischenknoten können die Kommunikation beliebig manipulieren. Dies verschärft sich in heterogenen Netzen, in denen Sicherheit auch über unterschiedliche Protokolle hinweg berücksichtigt werden muss. Zudem sollen Effizienzverluste an den Schnittstellen minimiert werden.

Die entworfene Verbindung soll prototypisch als Handy-Applikation (z.B. auf Android basierend) implementiert werden.

Kontakt: Markus Maron (B218, maron@uni-koblenz.de).


Testen von Verifikations-Werkzeugen


Kategorie: Diplomarbeit

Keywords: Softwareverifikation, Testen, Verifying C Compiler

Ziel der Softwareverifikation ist ein Beweis der Korrektheit eines Programms bezüglich seiner Spezifikation. Die bei der Verifikation verwendenten Werkzeuge werden jedoch in der Regel nicht selbst dem Prozess der Verifikation unterworfen, sondern deren Korrektheit wird als gegeben angenommen.

Ein Ansatz, die Qualität der verwendeten Werkzeuge zu überprüfen, ohne eine relativ aufwendige Verifikation des Werkzeugs durchzuführen, sind Softwaretests.

Im BMBF-Projekt VerisoftXT wird zur Verifikation von C-Code der Verifying C Compiler (VCC) von Microsoft Research eingesetzt. Da dieser im Rahmen des Projektes stetig weiterentwickelt wird, treten häufig Änderungen an dessen Implementierung und am Verifikations-Formalismus auf. Zudem ist die Implementierung des VCC für den Benutzer nicht verfügbar, so dass der Compiler als "black box" eingesetzt wird. Unter diesen Umständen ist es unpraktikabel einen eventuellen Beweis für die korrekte Arbeitsweise des VCC aktuell zu halten.

Ziel dieser Arbeit ist es, ausgehend von Resultaten aus dem Compiler-Testen, die Methodik des Testens auf Verifikationssysteme zu übertragen. Die theoretischen Ergebnisse sollen in einer Test-Suite für VCC umgesetzt werden. Diese Test Suite kann dann zum Regressions-Testen eingesetzt werden.

Kontakt: Thorsten Bormer ( tbormer@uni-koblenz.de )


Verifikation von Algorithmen-Implementationen


Kategorie: Diplomarbeit

Keywords: Formale Verifikation, Algorithmen, KeY

Algorithmen wie Dijkstras Kürzeste-Wege-Algorithmus werden in der Praxis häufig verwendet. Ihre Korrektheit ist aber meist nur in abstrakter Form mathematisch bewiesen. Diese Arbeit hat zum Ziel, Implementationen von Algorithmen mit dem Verifikationstool KeY zu verifizieren. Außerdem sollen dem Implementierer mögliche Optimierungsstellen aufgezeigt werden, soweit sich diese anhand des Beweises erkennen lassen.

Kontakt: Volker Klasen (reklov@uni-koblenz.de).

Betreuer: Bernhard Beckert


Using formal specifications for Common Criteria Certification


Kategorie: Studienarbeit

Keywords: Formale Verifikation, Zertifizierung, KeY

Das Thema der Studienarbeit umfasst das Gebiet der Softwarezertifizierung. Einer der prominenteren Standards für das Zertifizieren von Software unter Sicherheitskriterien (Security) ist die Common Criteria. Zwei Bestandteile der Common Criteria sind das Security Target und das Protection Profile.

Ziel der Studienarbeit ist es, zu untersuchen ob sich Teile des Zertifikats der CC aus vorhandenen Beweisartefakten und Spezifikationen generieren lassen.

Dies soll beispielhaft fuer eine Implementierung untersucht werden, fuer die Eigenschaften mit Hilfe des Programmverifikationstools KeY ( www.key-project.org ) bewiesen wurden.

Kontakt: Sarah Grebing (sarahgrebing@uni-koblenz.de).

Betreuer: Bernhard Beckert