Korrektheit und deren Durchsetzung im Umfeld langdauernder Abläufe

Abstract

In der vorliegenden Dissertation wird ein Modell erarbeitet, um transaktionale Eigenschaften, wie man sie aus dem Datenbankbereich kennt, auf langdauernde Abläufe übertragen zu können. Insbesondere fokusiert die Arbeit dabei auf den Problembereich des parallelen Zugriffs auf dieselben Datenobjekte. Zur formalen Beschreibung langlebiger Abläufe geht der vorgestellte Ansatz davon aus, dass ein Ablauf mit Hilfe des sogenannten ConTract-Modells beschrieben werden kann. Für diese Abläufe wird eine Transformation auf eine formale Notation bzw. eine formale Ausführungsmaschine erarbeitet und ein Historienbegriff definiert, der dem transaktionalen Historienbegriff ähnelt. Hierauf aufbauend wird eine Korrektheitsbegriff erarbeitet, der es erlaubt über die Korrektheit von Abläufen zu entscheiden. Anschließend beschäftigt sich die Arbeit mit der Umsetzung des Korrektheitsbegriffs in ein Laufzeitsystem zur Sicherstellung der Korrektheit. Es wird dabei speziell auf die Aspekte eingangen, die sich bei einer Einbettung der Mechanismen in das prototypisch vorliegende Laufzeittsystem von ConTracts (APRICOTS) ergeben. Insbesondere werden hier die Aspekte der Verteilung und der Ausfallsicherheit diskutiert. Die Arbeit schliesst mit der Identifikation offener Arbeitsgebiete sowie von Einschränkungen, die das ConTract-Modell noch aufweist. Es wird dabei deutlich, dass transaktional Zusicherungen nicht ohne Weiteres verallgemeinert werden können und möglicherweise neue Wege einzuschlagen sind, um weitere Anwendungsfelder entsprechend unterstützen zu können.

The given dissertation develops a model that allows the support of transactional properties for long-running applications. In particular, this work focuses on the area of concurrent access of shared data. To be able to fomally describe long-running processes it is assumed that a process can be modelled using the so-called ConTract model. For these processes, a transformation into a formal notation and a formal processing engine is introduced. Furthermore, the notion of a history is defined that is similar to histories in the transactional case. Based on this, the notion of correctness is defined that allows to decide the correctness of process executions. Continuing, the dissertation discusses the implementation of the notion of correctness by a runtime system that ensures the correctness. Particularly, aspects are discussed that arise while embedding the mechanism into the protypical runtime system of ConTracts (APRICOTS). Distribution and reliability are the amin aspects during this discussion. The dissertation closes with the identicfication of open points and of current restrictions of the ConTract model. It is shown that transactional guarantees cannot simply be used for all kinds of applications and that possibly new approaches have to be made to support futher applications.