Humboldt-Universität zu Berlin - Mathematisch-Naturwissenschaftliche Fakultät - Institut für Informatik

Probevortrag zur Promotion: Marvin Triebel

  • Wann 08.05.2018 von 13:15 bis 23:59
  • Wo Rudower Chaussee 25, Humboldt-Kabinett
  • iCal

Herr Marvin Triebel stellt am Dienstag, 8. Mai 2018 um 13.15 Uhr im Humboldt-Kabinett sein Promotionsvorhaben vor.

PRESERVING DATA INTEGRITY IN DISTRIBUTED SYSTEMS

Informationssysteme verarbeiten Daten, die logisch und physisch über viele Knoten verteilt sind. Datenobjekte verschiedener Knoten können dabei Bezüge zueinander haben. Beispielsweise kann ein Datenobjekt eine Referenz auf ein Datenobjekt eines anderen Knotens oder eine kritische Information wie ein Passwort enthalten. Die Semantik der Daten induziert Datenintegrität in Form von Anforderungen: Zum Beispiel sollte keine Referenz verwaist und kritische Informationen nur an einem Knoten verfügbar sein. Datenintegrität unterscheidet gültige von ungültigen, fehlerhaften Verteilungen der Daten. Wenn ein System Daten so verteilt, dass die Datenintegrität verletzt wird, ist es fehleranfällig.

Ein verteiltes System verändert sich in Schritten, die nebenläufig auftreten können. Jeder Schritt manipuliert Daten. Jede Manipulation erfolgt lokal und betrifft beschränkt viele Datenobjekte. Ein verteiltes System erhält Datenintegrität, wenn alle Schritte in einer Datenverteilung resultieren, die die Anforderungen von Datenintegrität erfüllen. Die Erhaltung von Datenintegrität ist daher ein notwendiges Korrektheitskriterium eines Systems. Der Entwurf und die Analyse von Datenintegrität in verteilten Systemen sind schwierig, weil ein verteiltes System nicht global kontrolliert werden kann, verschiedene Technologien eingesetzt werden und Daten unbeschränkt wachsen können.

In dieser Arbeit untersuchen wir formale Methoden für die Modellierung und Analyse verteilter Systeme, die mit Daten arbeiten. Wir entwickeln die Grundlagen für die Verifikation von Systemmodellen. Dazu verwenden wir algebraische Petrinetze. Wir zeigen, dass die Schritte verteilter Systeme mit endlichen vielen Transitionen eines algebraischen Petrinetzes beschrieben werden können, genau dann, wenn eine Schranke für die Bedingungen aller Schritte existiert. Wir verwenden algebraische Gleichungen und Ungleichungen, um Datenintegrität zu spezifizieren.
Wir zeigen zum einen, dass die Erhaltung von Datenintegrität unentscheidbar ist, wenn alle erreichbaren Schritte betrachtet werden. Und zum anderen zeigen wir, dass die Erhaltung von Datenintegrität entscheidbar ist, wenn auch unerreichbare Schritte berücksichtigt werden. Dies zeigen wir, indem wir die Berechenbarkeit eines nicht-erhaltenden Schrittes als Zeugen zeigen.

Sie sind herzlich dazu eingeladen.