Establishing Properties of Interaction Systems

Martens, Moritz

Vorschau

PDF
DrArbeitMyThesis.pdf - Veröffentlichte Version
Download (1MB)

URL:	https://ub-madoc.bib.uni-mannheim.de/2629
URN:	urn:nbn:de:bsz:180-madoc-26298
Dokumenttyp:	Dissertation
Erscheinungsjahr:	2009
Titel einer Zeitschrift oder einer Reihe:	None
Ort der Veröffentlichung:	Mannheim
Verlag:	Univ.
Hochschule:	Universität Mannheim
Gutachter:	Majster-Cederbaum, Mila
Datum der mündl. Prüfung:	18 Dezember 2009
Sprache der Veröffentlichung:	Englisch
Einrichtung:	Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik > Praktische Informatik II (Majster-Cederbaum -2005, Em)
Fachgebiet:	004 Informatik
Fachklassifikation:	CCS: F.1.2 Mode F.1.1 Mode ,
Normierte Schlagwörter (SWD):	Nebenläufigkeit , Komponente <Software> , Transitionssystem , Verklemmung , Fortschritt , Robustheit
Freie Schlagwörter (Deutsch):	hinreichende Bedingungen
Freie Schlagwörter (Englisch):	concurrency, component-based systems, deadlock-freedom, progress, robustness
Abstract:	We exhibit sufficient conditions for generic properties of component based systems. The model we use to describe component based systems is the formalism of interaction systems. Because the state space explosion problem is encountered in interaction systems (i.e., an exploration of the state space gets unfeasible for a large number of components), we follow the guideline that these conditions have to be checkable efficiently (i.e., in time polynomial in the number of components). Further, the conditions are designed in such a way that the information gathered is reusable if a condition is not satisfied. Concretely, we consider deadlock-freedom and progress in interaction systems. We state a sufficient condition for deadlock-freedom that is based on an architectural constraint: We define what it means for an interaction system to be tree-like, and we derive a sufficient condition for deadlock-freedom of such systems. Considering progress, we first present a characterization of this property. Then we state a sufficient condition for progress which is based on a directed graph. We combine this condition with the characterization to point out one possibility to proceed if the graph-criterion does not yield progress. Both sufficient conditions can be checked efficiently because they only require the investigation of certain subsystems. Finally, we consider the effect that failure of some parts of the system has on deadlock-freedom and progress. We define robustness of deadlock-freedom respectively progress under failure, and we explain how the sufficient conditions above have to be adapted in order to be also applicable in this new situation.
Übersetzter Titel:	Über den Nachweis von Eigenschaften von Interaktionssystemen (Deutsch)
Übersetzung des Abstracts:	Wir präsentieren hinreichende Bedingungen für allgemeine Eigenschaften von komponentenbasierten Systemen. Als Formalismus zur Modellierung komponentenbasierter Systeme nutzen wir Interaktionssysteme (interaction systems). Da für Interaktionssysteme das Problem der Zustandsraumexplosion auftritt (d.h. für eine große Anzahl von Komponenten ist eine Analyse des gesamten Zustandsraums nicht durchführbar), sollen die Bedingungen effizient überprüfbar sein (d.h. mit polynomiellem Aufwand in der Anzahl der Komponenten). Des Weiteren sind die Bedingungen so geartet, dass die gesammelte Information wiederbenutzbar ist, falls eine Bedingung nicht erfüllt sein sollte. Im Einzelnen betrachten wir Deadlockfreiheit und Fortschritt in Interaktionssystemen. Wir formulieren eine hinreichende Bedingung für Deadlockfreiheit, welche auf einer Einschränkung an die Kommunikationsarchitektur basiert: Wir definieren baumartige Interaktionssysteme und leiten dann eine hinreichende Bedingung für die Deadlockfreiheit solcher Systeme her. Im Hinblick auf Fortschritt geben wir zunachst eine Charakterisierung dieser Eigenschaft an. Dann formulieren wir basierend auf einem gerichteten Graphen eine hinreichende Bedingung für Fortschritt. Wir kombinieren diese Bedingung mit der Charakterisierung, um einen Ausweg aufzuzeigen, falls das Graphkriterium nicht erfüllt ist. Beide hinreichenden Bedingungen können effizient überprüft werden, weil nur die Analyse bestimmter Teilsysteme erforderlich ist. Schließlich untersuchen wir noch die Auswirkungen, welche der Ausfall bestimmter Teile eines Systems auf Deadlockfreiheit und Fortschritt hat. Wir definieren zunächst Robustheit von Deadlockfreiheit beziehungsweise Fortschritt unter Ausfall. Dann erklären wir, wie die obigen hinreichenden Bedingungen angepasst werden müssen, damit sie auf diese neue Situation angewendet werden können. (Deutsch)
Zusätzliche Informationen: