Correctness of services and their composition [Elektronische Ressource] / Niels Lohmann
189 Pages
English

Correctness of services and their composition [Elektronische Ressource] / Niels Lohmann

-

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

Description

CORRECTNESS OF SERVICESAND THEIR COMPOSITIONniels lohmannCopyright © 2010 by Niels Lohmann. Some rights reserved.This thesis is licensed under the Creative Commons Attribution-Noncommercial-ShareAlike 3.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by-nc-sa/3.0 or send a letter to Creative Commons, 171 Second Street, Suite 300,San Francisco, California, 94105, USA.A library record is available from the Eindhoven University of Technology Library.Lohmann, NielsCorrectness of services and their composition / by Niels Lohmann– Eindhoven: Technische Universiteit Eindhoven, 2010. – Proefschrift. –ISBN 978-90-386-2318-4NUR 993siks Dissertation Series No. 2010-37The research reported in this thesis has been carried out under the auspices of SIKS,theDutch Research School for Information and Knowledge Systems.The research reported in this theses has been partially supported by the dfg within grant“Operating Guidelines for Services” (WO 1466/8-1) and by the bmbf, project “Tools4BPEL”,project number 01ISE08.Printed by University Press Facilities, Eindhoven.Cover Design by Paul Verspaget.CORRECTNESS OF SERVICESAND THEIR COMPOSITIONPROEFSCHRIFTter verkrijging van de graad van doctor aan deTechnische Universiteit Eindhoven, op gezag van derector magnificus, prof.dr.ir. C.J. van Duijn, voor eencommissie aangewezen door het College voorPromoties in het openbaar te verdedigen opmaandag 27 september 2010 om 14.

Subjects

Informations

Published by
Published 01 January 2010
Reads 42
Language English
Document size 2 MB

CORRECTNESS OF SERVICES
AND THEIR COMPOSITION
niels lohmannCopyright © 2010 by Niels Lohmann. Some rights reserved.
This thesis is licensed under the Creative Commons Attribution-Noncommercial-Share
Alike 3.0 Unported License. To view a copy of this license, visit http://creativecommons.org/
licenses/by-nc-sa/3.0 or send a letter to Creative Commons, 171 Second Street, Suite 300,
San Francisco, California, 94105, USA.
A library record is available from the Eindhoven University of Technology Library.
Lohmann, Niels
Correctness of services and their composition / by Niels Lohmann
– Eindhoven: Technische Universiteit Eindhoven, 2010. – Proefschrift. –
ISBN 978-90-386-2318-4
NUR 993
siks Dissertation Series No. 2010-37
The research reported in this thesis has been carried out under the auspices of SIKS,the
Dutch Research School for Information and Knowledge Systems.
The research reported in this theses has been partially supported by the dfg within grant
“Operating Guidelines for Services” (WO 1466/8-1) and by the bmbf, project “Tools4BPEL”,
project number 01ISE08.
Printed by University Press Facilities, Eindhoven.
Cover Design by Paul Verspaget.CORRECTNESS OF SERVICES
AND THEIR COMPOSITION
PROEFSCHRIFT
ter verkrijging van de graad van doctor aan de
Technische Universiteit Eindhoven, op gezag van de
rector magnificus, prof.dr.ir. C.J. van Duijn, voor een
commissie aangewezen door het College voor
Promoties in het openbaar te verdedigen op
maandag 27 september 2010 om 14.00 uur
door
Niels Lohmann
geboren te Bonn, DuitslandDit proefschrift is goedgekeurd door de promotoren:
prof.dr.ir. W.M.P. van der Aalst
en
Prof.Dr. K. WolfCORRECTNESS OF SERVICES
AND THEIR COMPOSITION
DISSERTATION
zur
Erlangung des akademischen Grades
Doktor-Ingenieur (Dr.-Ing.)
der Faktultät für Informatik und Elektrotechnik
der Universität Rostock
vorgelegt von
Niels Lohmann, geboren am 10. Mai 1981 in Bonn
aus Rostock
Rostock, 4. Mai 2010
urn:nbn:de:gbv:28-diss2010-0138-3Gutachter:
1. Prof. Dr. Karsten Wolf
Universität Rostock
2. prof.dr.ir. Wil M. P. van der Aalst
Technische Universiteit Eindhoven
3. Prof. Dr. Mathias Weske
Hasso-Plattner-Institut an der Universität Potsdam
Datum der Verteidigung: Montag, 27. September 2010CORRECTNESS OF SERVICES AND THEIR COMPOSITION
abstract
Service-oriented computing (soc) is an emerging paradigm of system design and
aims at replacing complex monolithic systems by a composition of interacting systems,
called services. A service encapsulates self-contained functionality and offers it over
a well-defined, standardized interface.
This modularization may reduce both complexity and cost. At the same time, new
challenges arise with the distributed execution of services in dynamic compositions.
In particular, the correctness of a service composition depends not only on the local
correctness of each participating service, but also on the correct interaction between
them. Unlike in a centralized monolithic system, services may change and are not
completely controlled by a single party.
We study correctness of services and their composition and investigate how the
design of correct service compositions can be systematically supported. We thereby
focus on the communication protocol of the service and approach these questions
using formal methods and make contributions to three scenarios of soc.
The correctness of a service composition depends on the correctness of the partici-
pating services. To this end, we (1) study correctness criteria which can be expressed
and checked with respect to a single service. We validate services against behavioral
specifications and verify their satisfaction in any possible service composition. In case
a service is incorrect, we provide diagnostic information to locate and fix the error.
In case every participating service of a service composition is correct, their in-
teraction can still introduce problems. We (2) automatically verify correctness of
service compositions. We further support the design phase of service compositions
and present algorithms to automatically complete partially specified compo
and to fix incorrect compositions.
A service composition can also be derived from a specification, called choreography.
A choreography globally specifies the observable behavior of a composition. We (3)
present an algorithm to deduce local service descriptions from the choreography
which —by design — conforms to the specification.
All results have been expressed in terms of a unifying formal model. This not only
allows to formally prove correctness, but also makes results independent of the specifics
of concrete service description languages. Furthermore, all presented algorithms have
been prototypically implemented and validated in experiments based on case studies
involving industrial services.
7kurzfassung
Service-oriented Computing (soc) ist ein Paradigma des Systementwurfes mit dem
Ziel, komplexe monolithische Systeme durch eine Komposition von interagierenden
Systemen zu ersetzen. Diese interagierenden Systeme werden Services genannt und
kapseln in sich abgeschlossene Funktionen, die sie über eine wohldefinierte und stan-
dardisierte Schnittstelle anbieten.
Diese Modularisierung vermag Komplexität und Kosten zu senken. Gleichzeitig
führt die verteilte Ausführung von Services in dynamischen Kompositionen zu neuen
Herausforderungen. Dabei spielt Korrektheit eine zentrale Rolle, da sie nicht nur von
der lokalen Korrektheit der teilnehmenden Services, sondern auch von der Interaktion
zwischen den Services abhängt. Weiterhin können sich Services im Gegensatz zu
monolithischen Systemen verändern und werden nicht von einem einzelnen Teilnehmer
kontrolliert.
Wir studieren die Korrektheit von Services und Servicekompositionen und untersu-
chen, wie der Entwurf von korrekten Servicekompositionen systematisch unterstützt
werden kann. Wir legen dabei den Fokus auf das Kommunikationsprotokoll der Ser-
vices. Mithilfe von formalen Methoden tragen wir zu drei Szenarien von soc bei.
Die Korrektheit einer Servicekomposition hängt von der Korrektheit der teilneh-
menden Services ab. Aus diesem Grund (1) studieren wir Korrektheitseigenschaften,
die im Bezug auf einen einzelnen Service ausgedrückt und überprüft werden können.
Wir validieren Services gegen Verhaltensspezifikationen und verifizieren ihre Gültigkeit
in jeder möglichen Servicekomposition. Falls ein Service inkorrekt ist, erarbeiten wir
Diagnoseinformationen mit deren Hilfe Fehler lokalisiert und repariert werden können.
Falls alle teilnehmenden Services einer Servicekomposition korrekt sind, kann ih-
re Interaktion zu Problemen führen. Wir (2) verifizieren automatisch die Korrekt-
heit von Servicekompositionen. Weiterhin unterstützen wir die Entwurfsphase von
Servicekompositionen und stellen Algorithmen vor, mit denen teilweise spezifizierte
Kompositionen automatisch vervollständigt und mit denen inkorrekte Kompositionen
automatisch korrigiert werden können.
Eine Servicekomposition kann weiterhin von einer Spezifikation (Choreographie ge-
nannt) abgeleitet werden. Eine Choreographie spezifiziert den Nachrichtenaustausch
in einer Servicekomposition. Wir (3) erarbeiten einen Algorithmus, mit dem lokale
Servicebeschreibungen aus einer abgeleitet werden können, die per
Konstruktion der Spezifikation genügen.
Alle Resultate wurden in einem einheitlichen formalen Modell ausgedrückt. Dies
ermöglicht nicht nur formale Beweise, sondern macht die Resultate von konkreten
Spezifikationssprachen unabhängig. Weiterhin wurden alle vorgestellten Algorithmen
prototypisch implementiert und anhand von industriellen Fallstudien validiert.
8CONTENTS
1 Introduction 11
1.1 Research goal 15
1.2 Contributions 16
1.3 Outline 19
2 Formal models for services 21
2.1 Preliminaries 21
2.2 Modeling services and their composition 23
2.3 Correctness notions for services 26
2.4 Construction of strategies 29
2.5 Finite characterization of strategies 32
2.6 Experimental Results 35
2.7 Discussion 36
i correctness of services 41
3 Validation and selection 43
3.1 Intended and unintended behavior 43
3.2 Adding constraints to service automata 45
3.3 Addingts to operating guidelines 49
3.4 Implementation and experimental results 53
3.5 Discussion and related work 55
3.6 Conclusion 57
4 Diagnosis 59
4.1 Reasons for uncontrollability 59
4.2 Counterexamples for controllability 64
4.3 An overapproximation of a counterexample 68
4.4 Blacklist-based diagnosis 70
4.5 Diagnosis algorithm 74
4.6 Conclusion 76
ii correctness of service compositions 79
5 Verification and Completion 81
5.1 WS-BPEL and BPEL4Chor 83
5.2 Formalizing WS-BPEL and BPEL4Chor 87
5.3 Analyzing closed choreographies 94
5.4 Completing Choreographies 100
5.5 Related Work 103
5.6 Conclusion 104
9contents
6 Correction 107
6.1 Motivating example 108
6.2 Correcting incompatible choreographies 110
6.3 Graph similarities 112
6.4 A matching-based edit distance 115
6.5 Experimental results 125
6.6 Related work 127
6.7 Conclusion and Future Work 129
iii correctness of service choreographies 131
7 Realizability 133
7.1 Modeling choreographies 134
7.2 Realizability notions 137
7.3 Realizing choreographies 139
7.4 asynchronous communication 146
7.5 Combining interaction models and interconnected models 148
7.6 Related Work 149
7.7 Conclusion 152
8 Conclusions 155
8.1 Summary of contributions 155
8.2 Classification of con 157
8.3 Limitations and open problems 160
8.4 Future work 161
Theses 163
Bibliography 165
Glossary 175
Statement 177
Curriculum vitæ 178
Acknowledgments 181
SIKS Dissertations 183
10