CSP as a Coordination Language. A CSP-based Approach to the Coordination of Concurrent Systems
| dc.contributor.advisor | Jähnichen, Stefan | en |
| dc.contributor.author | Kleine, Moritz | en |
| dc.contributor.grantor | Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik | en |
| dc.date.accepted | 2011-06-24 | |
| dc.date.accessioned | 2015-11-20T20:45:19Z | |
| dc.date.available | 2011-10-18T12:00:00Z | |
| dc.date.issued | 2011-10-18 | |
| dc.date.submitted | 2011-10-18 | |
| dc.description.abstract | Die Beherrschbarkeit komplexer nebenläufiger Systeme hängt in hohem Maße davon ab, mit welchen Methoden das System modelliert bzw. spezifiziert wird. Formale auf Nebenläufigkeit spezialisierte Methoden erlauben es, solche Systeme elegant auf einem hohen Abstraktionsniveau zu modellieren und zu analysieren. Ein Vertreter derartiger Methoden ist die in dieser Arbeit verwendete Prozess Algebra CSP. CSP ist ein weitverbreiteter, wohluntersuchter Formalismus, der es erlaubt, ein nebenläufiges System mathematisch präzise zu beschreiben und wichtige Eigenschaften, beispielsweise Verklemmungsfreiheit, zu verifizieren. Dennoch ist die Ableitung einer Systemimplementierung aus einem gegebenen CSP Modell immer noch ein aktueller Forschungsgegenstand. So ist zum Beispiel unklar, wie interne Aktionen eines Systems in einer Implementierung integriert werden können, da diese in CSP ununterscheidbar sind. Als Lösung wird in dieser Arbeit vorgeschlagen, CSP mit einer sequentiellen Zielsprache zu integrieren, so dass die Aktionen eines Systems in der sequentiellen Zielsprache implementiert werden und die Aktionen entsprechend eines CSP Prozesses koordiniert werden. Koordinationssprachen zielen ebenfalls darauf ab, Nebenläufigkeit von sequentiellen Aspekten eines Systems zu trennen, sie sind aber weniger auf automatisierte formale Verifikation ausgerichtet. In der Arbeit wird die Verwendung der Prozess Algebra CSP als formale Koordinationssprache für beliebige sequentielle Zielsprachen vorgeschlagen. Hierfür wird das formale Fundament einer Koordinationsumgebung entwickelt, die einen CSP Prozess zur Laufzeit simuliert und die Aktionen des Systems entsprechend ausführt. Besonderer Wert liegt auf der Koordination interner Aktionen und auf der Erkennung von Nebenläufigkeit zwischen extern synchronisierbaren und internen Aktionen. Durch Beweisverpflichtungen wird der Zusammenhang zwischen dem Koordinationsprozess und den Implementierungen der Aktionen hergestellt. Die Koordinationsumgebung wird konkret für die Zielsprache Java implementiert. Desweiteren wird eine Fallstudie vorgestellt, die sich mit der Entwicklung eines Workflow Servers beschäftigt, dessen interne Nebenläufigkeit einerseits selbst mittels CSP koordiniert wird und der andererseits CSP-basierte Workflows ausführen kann, die ebenfalls durch eine CSP Koordinationsumgebung gesteuert werden. Die Arbeit enthält wissenschaftliche Beiträge zur Theorie und der praktischen Verwendbarkeit von CSP, bezüglich der Konstruktion korrekter nebenläufiger Systeme, sowie zum Bereich der Modellierung und Verwaltung von Workflows. | de |
| dc.description.abstract | Complex concurrent systems are in general hard to understand, and equally hard to specify and to verify. The process algebra Communicating Sequential Processes (CSP) offers a way of taming the complexity of concurrent systems by focusing on the interaction behavior of systems and abstracting from synchronization mechanisms and other implementation details. CSP provides a mature intermediate level formalism that allows us to specify and model such systems in a mathematically precise way and to verify important properties, e. g., deadlock-freedom. However, the derivation of a system’s implementation from its CSP-based model is still a problem and sub ject to ongoing research. It is, for example, not obvious how to integrate CSP with internal actions of a system, because CSP abstracts from internal actions to a great extent. To overcome this problem, we propose to integrate CSP with a sequential host language such that the concurrency aspects of systems are captured on the CSP level and its actions are implemented in the sequential host language. This idea of separating concurrent and sequential aspects of a system is also known from coordination languages, but those are in general less amenable to automated verification. In this thesis, we present the use of CSP as a formal coordination language for arbitrary sequential host languages, allowing us to use CSP for the design, implementation, and verification of concurrent systems. To this end, we develop the model of a coordination environment that simulates a CSP process at runtime and performs the system’s actions accordingly. The coordination environment controls the system’s interaction with its environment as well as its internal actions. We present proof obligations to ensure that the properties proved on the CSP level also hold on the implementation level of the system. We also present an implementation of the coordination environment for the target language Java and a case study of constructing a workflow server as a coordinated concurrent Java program. This thesis contributes to the theory and practice of CSP, to the engineering of correct concurrent systems, and to the modeling and management of workflows. The main contribution of this thesis is a target language independent CSP-based framework for the construction of provably correct concurrent systems. | en |
| dc.identifier.uri | urn:nbn:de:kobv:83-opus-32169 | |
| dc.identifier.uri | https://depositonce.tu-berlin.de/handle/11303/3265 | |
| dc.identifier.uri | http://dx.doi.org/10.14279/depositonce-2968 | |
| dc.language | English | en |
| dc.language.iso | en | en |
| dc.rights.uri | http://rightsstatements.org/vocab/InC/1.0/ | en |
| dc.subject.ddc | 004 Datenverarbeitung; Informatik | en |
| dc.subject.other | CSP | de |
| dc.subject.other | Formale Sprachen | de |
| dc.subject.other | Koordinationssprachen | de |
| dc.subject.other | Nebenläufigkeit | de |
| dc.subject.other | Workflows | de |
| dc.subject.other | Concurrency | en |
| dc.subject.other | Coordination Languages | en |
| dc.subject.other | CSP | en |
| dc.subject.other | Formal Languages | en |
| dc.subject.other | Workflows | en |
| dc.title | CSP as a Coordination Language. A CSP-based Approach to the Coordination of Concurrent Systems | en |
| dc.type | Doctoral Thesis | en |
| dc.type.version | publishedVersion | en |
| tub.accessrights.dnb | free | * |
| tub.affiliation | Fak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.affiliation.faculty | Fak. 4 Elektrotechnik und Informatik | de |
| tub.affiliation.institute | Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.identifier.opus3 | 3216 | |
| tub.identifier.opus4 | 3054 | |
| tub.publisher.universityorinstitution | Technische Universität Berlin | en |
Files
Original bundle
1 - 1 of 1