Informationssysteme verarbeiten Daten, die logisch und physisch über 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 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 Verteilungen der Daten.
Ein verteiltes System verändert sich in Schritten, die nebenläufig auftreten können. Jeder Schritt manipuliert Daten. 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.
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, dass die Erhaltung von Datenintegrität unentscheidbar ist, wenn alle erreichbaren Schritte betrachtet werden. Und wir zeigen, 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. / Information systems process data that is logically and physically distributed over many locations. Data entities at different locations may be in a specific relationship. For example, a data entity at one location may contain a reference to a data entity at a different location, or a data entity may contain critical information such as a password. The semantics of data entities induce data integrity in the form of requirements. For example, no references should be dangling, and critical information should be available at only one location. Data integrity discriminates between correct and incorrect data distributions.
A distributed system progresses in steps, which may occur concurrently. In each step, data is manipulated. Each data manipulation is performed locally and affects a bounded number of data entities. A distributed system preserves data integrity if each step of the system yields a data distribution that satisfies the requirements of data integrity. Preservation of data integrity is a necessary condition for the correctness of a system. Analysis and design are challenging, as distributed systems lack global control, employ different technologies, and data may accumulate unboundedly.
In this thesis, we study formal methods to model and analyze distributed data-aware systems. As a result, we provide a technology-independent framework for design-time analysis. To this end, we use algebraic Petri nets. We show that there exists a bound for the conditions of each step of a distributed system if and only if the steps can be described by a finite set of transitions of an algebraic Petri net. We use algebraic equations and inequalities to specify data integrity. We show that preservation of data integrity is undecidable in case we consider all reachable steps. We show that preservation of data integrity is decidable in case we also include unreachable steps. We show the latter by showing computability of a non-preserving step as a witness.
| Identifer | oai:union.ndltd.org:HUMBOLT/oai:edoc.hu-berlin.de:18452/20360 |
| Date | 30 November 2018 |
| Creators | Triebel, Marvin |
| Contributors | Reisig, Wolfgang, Montali, Marco, Weske, Mathias |
| Publisher | Humboldt-Universität zu Berlin |
| Source Sets | Humboldt University of Berlin |
| Language | English |
| Detected Language | English |
| Type | doctoralThesis, doc-type:doctoralThesis |
| Format | application/pdf |
| Rights | (CC BY-NC-ND 3.0 DE) Namensnennung - Nicht-kommerziell - Keine Bearbeitung 3.0 Deutschland, http://creativecommons.org/licenses/by-nc-nd/3.0/de/ |
Page generated in 0.0025 seconds