Publikationen des Jahres 2007
Dissertationen und Habilitationen
Bixia Wu. Entwurf und Verifikation von Petrinetzmodellen verteilter Algorithmen durch Verfeinerung unverteilter Algorithmen. Dissertation, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, July 2007.
Abstract: Um Entwurf und Verifikation komplizierter verteilter Algorithmen leichter und verständlicher zu machen, wird oft eine Verfeinerungsmethode verwendet. Dabei wird ein einfacher Algorithmus, der gewünschte Eigenschaften erfüllt, schrittweise zu einem komplizierten Algorithmus verfeinert. In jedem Schritt sollen die gewünschten Eigenschaften erhalten bleiben. Für nachrichtenbasierte verteilte Algorithmen haben wir eine neue Verfeinerungsmethmode entwickelt. Wir beginnen mit einem Anfangsalgorithmus, der Aktionen enthält, die gemeinsame Aufgaben mehrerer Agenten beschreiben. In jedem Schritt verfeinern wir eine dieser Aktionen zu einem Netz, das nur solche Aktionen enthält, die die Aufgaben einzelner Agenten beschreiben. Jeder Schritt ist also eine Verteilung einer unverteilten Aktion. Die Analyse solcher Verfeinerungsschritte wird mit Hilfe eines neuen Verfeinerungsbegriffs - der verteilenden Verfeinerung - durchgeführt. Entscheidend dabei ist das Erhaltenbleiben der Halbordnungen des zu verfeinernden Algorithmus. Dies ist durch Kausalitäten der Aktionen der Agenten im lokalen Verfeinerungsnetz zu erreichen. Die Kausalitäten im lokalen Verfeinerungsnetz lassen sich einerseits beim Entwurf direkt durch Nachrichtenaustausch realisieren. Andererseits kann man bei der Verifikation die Gültigkeit einer Kausalität im lokalen Verfeinerungsnetz direkt vom Netz ablesen. Daher ist diese Methode leicht zu verwenden. Die Anwendung der Methode wird in der Arbeit an verschiedenen nicht trivialen Beispielen demonstriert. @PhDThesis{Wu2007_diss, author = {Bixia Wu}, title = {{Entwurf und Verifikation von Petrinetzmodellen verteilter Algorithmen durch Verfeinerung unverteilter Algorithmen}}, school = {Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II}, year = 2007, type = {Dissertation}, month = jul, pdf = {http://edoc.hu-berlin.de/dissertationen/wu-bixia-2007-06-22/PDF/wu.pdf}, url = {http://edoc.hu-berlin.de/docviews/abstract.php?lang=ger&id=28034}, abstract = {Um Entwurf und Verifikation komplizierter verteilter Algorithmen leichter und verständlicher zu machen, wird oft eine Verfeinerungsmethode verwendet. Dabei wird ein einfacher Algorithmus, der gewünschte Eigenschaften erfüllt, schrittweise zu einem komplizierten Algorithmus verfeinert. In jedem Schritt sollen die gewünschten Eigenschaften erhalten bleiben. Für nachrichtenbasierte verteilte Algorithmen haben wir eine neue Verfeinerungsmethmode entwickelt. Wir beginnen mit einem Anfangsalgorithmus, der Aktionen enthält, die gemeinsame Aufgaben mehrerer Agenten beschreiben. In jedem Schritt verfeinern wir eine dieser Aktionen zu einem Netz, das nur solche Aktionen enthält, die die Aufgaben einzelner Agenten beschreiben. Jeder Schritt ist also eine Verteilung einer unverteilten Aktion. Die Analyse solcher Verfeinerungsschritte wird mit Hilfe eines neuen Verfeinerungsbegriffs - der verteilenden Verfeinerung - durchgeführt. Entscheidend dabei ist das Erhaltenbleiben der Halbordnungen des zu verfeinernden Algorithmus. Dies ist durch Kausalitäten der Aktionen der Agenten im lokalen Verfeinerungsnetz zu erreichen. Die Kausalitäten im lokalen Verfeinerungsnetz lassen sich einerseits beim Entwurf direkt durch Nachrichtenaustausch realisieren. Andererseits kann man bei der Verifikation die Gültigkeit einer Kausalität im lokalen Verfeinerungsnetz direkt vom Netz ablesen. Daher ist diese Methode leicht zu verwenden. Die Anwendung der Methode wird in der Arbeit an verschiedenen nicht trivialen Beispielen demonstriert.} }
Publikationen in Zeitschriften und Büchern
Wil M. P. van der Aalst, Michael Beisiegel, Kees M. van Hee, Dieter König, and Christian Stahl. An SOA-based architecture framework. International Journal of Business Process Integration and Management (IJBPIM), 2(2):91-101, 2007.
Abstract: We present an Service-Oriented Architecture (SOA)-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service ComponentArchitecture (SCA).The framework is language independent and the building blocks of each system, activities and data, are first class citizens.We present a meta model of the architecture framework and discuss its concepts in detail. Through the framework, concepts of an SOA such as wiring, correlation and instantiation can be clarified. @ARTICLE{AalstBHKS2007_ijbpim, AUTHOR = {{Wil} {M.} {P.} {van} {der} Aalst and Michael Beisiegel and {Kees} {M.} {van} Hee and Dieter K{\"o}nig and Christian Stahl}, TITLE = {{An SOA-based architecture framework}}, JOURNAL = {International Journal of Business Process Integration and Management (IJBPIM)}, YEAR = {2007}, volume = {2}, number = {2}, pages = {91-101}, keywords = {SOA, Architecture framework, SCA}, url = {http://dx.doi.org/10.1504/IJBPIM.2007.015132}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/AalstBHKS2007_ijbpim.pdf}, abstract = {We present an Service-Oriented Architecture (SOA)-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service ComponentArchitecture (SCA).The framework is language independent and the building blocks of each system, activities and data, are first class citizens.We present a meta model of the architecture framework and discuss its concepts in detail. Through the framework, concepts of an SOA such as wiring, correlation and instantiation can be clarified.} }Kathrin Kaschner, Peter Massuthe, and Karsten Wolf. Symbolic Representation of Operating Guidelines for Services. Petri Net Newsletter, 72:21-28, April 2007.
@Article{KaschnerMW2007_pnn72, author = {Kathrin Kaschner and Peter Massuthe and Karsten Wolf}, title = {{Symbolic Representation of Operating Guidelines for Services}}, journal = {Petri Net Newsletter}, year = 2007, volume = 72, pages = {21-28}, month = apr, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/KaschnerMW2007_pnn72.pdf}, keywords = {Services, Operating Guidelines, BDD} }Peter Massuthe and Karsten Wolf. An Algorithm for Matching Non-deterministic Services with Operating Guidelines. International Journal of Business Process Integration and Management (IJBPIM), 2(2):81-90, 2007.
Abstract: Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requesters service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented. @article{MassutheW2007_ijbpim, author = {Peter Massuthe and Karsten Wolf}, title = {{An Algorithm for Matching Non-deterministic Services with Operating Guidelines}}, journal = {International Journal of Business Process Integration and Management (IJBPIM)}, year = 2007, volume = 2, number = 2, pages = {81-90}, keywords = {Services, Operating Guidelines, Matching}, abstract = {Interorganisational cooperation is more and more organised by the paradigm of services. Service-Oriented Architectures (SOA) provide a general framework for service interaction. SOA describe three roles of services, the service provider, the service requester and the service broker, together with the three operations publish, find and bind. We provide a formal method based on non-deterministic automata to model services and their interaction. In this paper, we restrict ourselves to finite and acyclic automata. We suggest operating guidelines as a convenient and intuitive artefact to realise the publish operation. In our approach, the find operation reduces to a matching problem between the requesters service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free interaction. In this paper, matching of deterministic as well as non-deterministic automata with operating guidelines is presented.} }Wolfgang Reisig. The Decent Philosophers: An Exercise in Concurrent Behaviour. Fundamenta Informaticae, 80(1-3):273-281, November 2007.
Abstract: Concurrent runs reveal more insight into distributed systems than interleaved runs. This is shown by help of Dijkstra's paradigm of five philosophers. @Article{Reisig2007_tdpaeicb, author = {Wolfgang Reisig}, title = {{The Decent Philosophers: An Exercise in Concurrent Behaviour}}, journal = {Fundamenta Informaticae}, year = 2007, Month = nov, Number = {1-3}, Pages = {273-281}, Volume = {80}, keywords = {Petrinetze}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Reisig2007_tdpaeicb.pdf}, url = {http://fi.mimuw.edu.pl/abs80.html#14}, abstract = {Concurrent runs reveal more insight into distributed systems than interleaved runs. This is shown by help of Dijkstra's paradigm of five philosophers.} }Wolfgang Reisig, Karsten Wolf, Jan Bretschneider, Kathrin Kaschner, Niels Lohmann, Peter Massuthe, and Christian Stahl. Challenges in a Service-Oriented World. ERCIM News, 70:28-29, July 2007.
Abstract: Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services. @article{ReisigWBKLMS2007_ercim, Author = {Wolfgang Reisig and Karsten Wolf and Jan Bretschneider and Kathrin Kaschner and Niels Lohmann and Peter Massuthe and Christian Stahl}, Journal = {ERCIM News}, Month = jul, volume = {70}, Pages = {28-29}, Title = {Challenges in a Service-Oriented World}, URL = {http://ercim-news.ercim.org/content/view/213/408}, Year = {2007}, Abstract = {Interacting services raise a number of new software engineering challenges. To meet these challenges, the behaviour of the involved services must be considered. We present results regarding the behaviour of services in isolation, the interaction of services in choreographies, the exchangeability of a service, and the synthesis of desired partner services.} }
Konferenzbeiträge und Beiträge auf Workshops
Dirk Fahland. A Formal Approach to Adaptive Processes using Scenario-based Concepts.. In Kees van Hee, Wolfgang Reisig, and Karsten Wolf, editors, Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), Siedlce, Poland, pages 71--85, June 2007. University of Podlasie.
Abstract: The problem and need for adapting business processes and service behavior to cope with changing circumstances is identified well. Standard models for business processes still rely on a fixed process logic, the change of which is rather hard to achieve. Ad-hoc changes to a standard model are usually considered too `dangerous' as they are performed in not well-defined manner. Other models for adaptive processes deviate to some extent from established business process models. This deviation comes at the price of limited understandability and loss in analysis capabilities. We propose a model for adaptive processes based on Petri nets which have successfully been applied in modeling and analyzing business process and web services. Our operator to adapt the behavior of such models is formalized by the help of scenario-based concepts known from live-sequence charts in purely mathematical terms. This combination of concepts allows to write down the result of the adaptation rather than how adaptation shall be performed. @INPROCEEDINGS{Fahland2007_fabpws, author = {Dirk Fahland}, title = {{A Formal Approach to Adaptive Processes using Scenario-based Concepts.}}, booktitle = {{Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07)}}, year = {2007}, editor = {Kees {van} Hee and Wolfgang Reisig and Karsten Wolf}, pages = {71--85}, address = {Siedlce, Poland}, month = {jun}, publisher = {University of Podlasie}, keywords = {Adaptive/Flexible Workflows, Szenario-basierte Modelle, oWFNs}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Fahland2007_fabpws.pdf}, abstract = {The problem and need for adapting business processes and service behavior to cope with changing circumstances is identified well. Standard models for business processes still rely on a fixed process logic, the change of which is rather hard to achieve. Ad-hoc changes to a standard model are usually considered too `dangerous' as they are performed in not well-defined manner. Other models for adaptive processes deviate to some extent from established business process models. This deviation comes at the price of limited understandability and loss in analysis capabilities. We propose a model for adaptive processes based on Petri nets which have successfully been applied in modeling and analyzing business process and web services. Our operator to adapt the behavior of such models is formalized by the help of scenario-based concepts known from live-sequence charts in purely mathematical terms. This combination of concepts allows to write down the result of the adaptation rather than how adaptation shall be performed.} }Dirk Fahland. Modeling and Verifying Declarative Workflows. In Dagstuhl ''zehn plus eins'', Aachen, pages 135, 2007. Verlagshaus Mainz.
@INPROCEEDINGS{Fahland_2007_dagstuhl07232, author = {Fahland, Dirk}, title = {{Modeling and Verifying Declarative Workflows}}, booktitle = {Dagstuhl ''zehn plus eins''}, year = {2007}, pages = {135}, address = {Aachen}, publisher = {Verlagshaus Mainz}, keywords = {Adaptive/Flexible Workflows, Szenario-basierte Modelle, Petrinetze, Deklarative Modelle, Temporale Logik} }Dirk Fahland. Synthesizing Petri nets from LTL specifications - An engineering approach. In Stephan Philippi and Alexander Pinl, editors, Proceedings 14.Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN), Arbeitsbericht aus dem Fach Informatik, Nr. 25/2007, Universität Koblenz-Landau, D, pages 69--74, September 2007.
Abstract: In this paper we present a pattern-based approach for synthesizing truly distributed Petri nets from a class of LTL specifications. The synthesis allows for the automatic, correct generation of humanly conceivable Petri nets, thus circumventing a manual construction of nets, or the use of Büuchi automata which are not distributed and often less intuitive to understand. @INPROCEEDINGS{Fahland2007_awpn, author = {Fahland, Dirk}, title = {{Synthesizing Petri nets from LTL specifications - An engineering approach}}, booktitle = {Proceedings 14.Workshop Algorithmen und Werkzeuge für Petrinetze (AWPN), Arbeitsbericht aus dem Fach Informatik, Nr. 25/2007}, editor = {Philippi, Stephan and Pinl, Alexander}, month = {September}, year = {2007}, address = {Universität Koblenz-Landau, D}, keywords = {Adaptive/Flexible Workflows, Deklarative Modelle, Petrinetze, Temporale Logik}, pages = {69--74}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Fahland2007_awpn.pdf}, abstract = {In this paper we present a pattern-based approach for synthesizing truly distributed Petri nets from a class of LTL specifications. The synthesis allows for the automatic, correct generation of humanly conceivable Petri nets, thus circumventing a manual construction of nets, or the use of Büuchi automata which are not distributed and often less intuitive to understand.} }Dirk Fahland. Towards Analyzing Declarative Workflows. In Jana Koehler, Marco Pistore, Amit P. Sheth, Paolo Traverso, and Martin Wirsing, editors, Autonomous and Adaptive Web Services, number 07061 of Dagstuhl Seminar Proceedings, 2007. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany.
Abstract: Enacting tasks in a workflow cannot always follow a pre-defined process model. In application domains like disaster management workflows are partially specified and circumstances of their enactment change. There exist various approaches for formal workflow models that are effective in such situations, like declarative specifications instead of operational models for formalizing flexible workflow process. These powerful models leave a gap to existing techniques in the domain of workflow modeling, workflow analysis, and workflow management. In this paper we bridge this gap with a compositional mechanism for translating declarative workflow models to operational workflow models. The mechanism is of a general nature and we reveal its principles as we provide an exemplary definition for translating DecSerFlow models based on LTL to Petri nets. We then demonstrate its use in analyzing and refining declarative models. @InProceedings{Fahland2007_dagstuhl07061, author = {Dirk Fahland}, title = {Towards Analyzing Declarative Workflows}, booktitle = {Autonomous and Adaptive Web Services}, year = {2007}, editor = {Jana Koehler and Marco Pistore and Amit P. Sheth and Paolo Traverso and Martin Wirsing}, number = {07061}, series = {Dagstuhl Seminar Proceedings}, ISSN = {1862-4405}, publisher = {Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany}, OPTaddress = {Dagstuhl, Germany}, url = {http://drops.dagstuhl.de/opus/volltexte/2007/1033}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Fahland2007_dagstuhl07061.pdf}, OPTannote = {Keywords: Adaptive/Flexible Workflow, Declarative Modeling, temporal logic, analysis, transformation, Petri nets}, abstract = {Enacting tasks in a workflow cannot always follow a pre-defined process model. In application domains like disaster management workflows are partially specified and circumstances of their enactment change. There exist various approaches for formal workflow models that are effective in such situations, like declarative specifications instead of operational models for formalizing flexible workflow process. These powerful models leave a gap to existing techniques in the domain of workflow modeling, workflow analysis, and workflow management. In this paper we bridge this gap with a compositional mechanism for translating declarative workflow models to operational workflow models. The mechanism is of a general nature and we reveal its principles as we provide an exemplary definition for translating DecSerFlow models based on LTL to Petri nets. We then demonstrate its use in analyzing and refining declarative models.}, Keywords = {Adaptive/Flexible Workflows, Deklarative Modelle, Petrinetze, Temporale Logik} }Dirk Fahland, Timo M. Gläßer, Bastian Quilitz, Stephan Weißleder, and Ulf Leser. HUODINI - Flexible Information Integration for Disaster Management. In 4th International Conference on Information Systems for Crisis Response and Management (ISCRAM), Delft, NL, 2007. Note: Revised version submitted to a special issue of IEEE DSonline.
Abstract: Fast and effective disaster management requires access to a multitude of heterogeneous, distributed, and quickly changing data sets, such as maps, satellite images, or governmental databases. In the last years, also the information created by affected persons on web sites such as flickr.com or blogger.com became an important and very quickly adapting source of information. We developed HUODINI, a prototype system for the flexible integration and visualization of heterogeneous data sources for disaster management. HUODINI is based on Semantic Web technologies, and in particular RDF, to offer maximal flexibility in the types of data sources it can integrate. It supports a hybrid push/pull approach to cater for the requirements of fast-changing sources, such as news feeds, and maximum performance for querying the integrated data set. In this paper, we describe the design goals underlying our approach, its architecture, and report on first experiences with the system. @INPROCEEDINGS{Fahland2007_huodini, author = {Fahland, Dirk and Gläßer, Timo M. and Quilitz, Bastian and Weißleder, Stephan and Leser, Ulf}, title = {{HUODINI - Flexible Information Integration for Disaster Management}}, booktitle = {4th International Conference on Information Systems for Crisis Response and Management (ISCRAM)}, year = {2007}, address = {Delft, NL}, pdf = {http://metrik.informatik.hu-berlin.de/grk-wiki/index.php/Publications:HUODINI_-_Flexible_Information_Integration_for_Disaster_Management}, note = {revised version submitted to a special issue of IEEE DSonline}, abstract = {Fast and effective disaster management requires access to a multitude of heterogeneous, distributed, and quickly changing data sets, such as maps, satellite images, or governmental databases. In the last years, also the information created by affected persons on web sites such as flickr.com or blogger.com became an important and very quickly adapting source of information. We developed HUODINI, a prototype system for the flexible integration and visualization of heterogeneous data sources for disaster management. HUODINI is based on Semantic Web technologies, and in particular RDF, to offer maximal flexibility in the types of data sources it can integrate. It supports a hybrid push/pull approach to cater for the requirements of fast-changing sources, such as news feeds, and maximum performance for querying the integrated data set. In this paper, we describe the design goals underlying our approach, its architecture, and report on first experiences with the system.} }Andreas Glausch. A Semantic Characterization of Elementary Wide-Step ASMs. In Proceedings of the 14th International ASM Workshop, June 2007.
@INPROCEEDINGS{Glausch2007_asm07, author = {Andreas Glausch}, title = {{A Semantic Characterization of Elementary Wide-Step ASMs}}, year = {2007}, booktitle = {Proceedings of the 14th International ASM Workshop}, url = {http://ikt.hia.no/asm07}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Glausch2007_asm07.pdf}, month = jun, keywords = {ASM} }Andreas Glausch and Wolfgang Reisig. A Semantic Characterization of Unbounded-Nondeterministic ASMs. In Proceedings of the 2nd Conference on Algebra and Coalgebra in Computer Science, volume 4624 of Lecture Notes in Computer Science, August 2007.
Abstract: Universal algebra usually considers and examines algebras as static entities. In the mid 80ies Gurevich proposed Abstract State Machines (ASMs) as a computation model that regards algebras as dynamic: a state of an ASM is represented by a freely chosen algebra which may change during a computation. In 2000, Gurevich characterized the class of sequential ASMs in a purely semantical way by five amazingly general and elegant axioms. Later this result has been extended to bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among unboundedly many (sometimes infinitely many) alternatives. We characterize the class of unbounded-nondeterministic ASMs by an extension of Gurevich's original axioms for sequential ASMs. We apply this result to prove the reversibility of unbounded-nondeterministic ASMs. @INPROCEEDINGS{GlauschR2007_calco, author = {Andreas Glausch and Wolfgang Reisig}, title = {{A Semantic Characterization of Unbounded-Nondeterministic ASMs}}, year = {2007}, month = aug, booktitle = {Proceedings of the 2nd Conference on Algebra and Coalgebra in Computer Science}, series = {Lecture Notes in Computer Science}, volume = {4624}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/GlauschR2007_calco.pdf}, keywords = {ASM}, abstract = { Universal algebra usually considers and examines algebras as static entities. In the mid 80ies Gurevich proposed Abstract State Machines (ASMs) as a computation model that regards algebras as dynamic: a state of an ASM is represented by a freely chosen algebra which may change during a computation. In 2000, Gurevich characterized the class of sequential ASMs in a purely semantical way by five amazingly general and elegant axioms. Later this result has been extended to bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among unboundedly many (sometimes infinitely many) alternatives. We characterize the class of unbounded-nondeterministic ASMs by an extension of Gurevich's original axioms for sequential ASMs. We apply this result to prove the reversibility of unbounded-nondeterministic ASMs. } }Andreas Glausch and Wolfgang Reisig. An ASM-Characterization of a Class of Distributed Algorithms. In Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, Festschrift volume of Lecture Notes in Computer Science, 2007. Springer. Note: To appear.
@inproceedings{GlauschR2007_dagstuhl, author = {Andreas Glausch and Wolfgang Reisig}, title = {{An ASM-Characterization of a Class of Distributed Algorithms}}, booktitle = {{Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis}}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/GlauschR2007_dagstuhl.pdf}, publisher = {Springer}, series = {Festschrift volume of Lecture Notes in Computer Science}, year = 2007, note = {{to appear}} }Niels Lohmann. A Feature-Complete Petri Net Semantics for WS-BPEL 2.0. In Kees van Hee, Wolfgang Reisig, and Karsten Wolf, editors, Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07), pages 21-35, June 2007. University of Podlasie.
Abstract: We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification. @inproceedings{Lohmann2007_fabpws, Author = {Niels Lohmann}, Booktitle = {Proceedings of the Workshop on Formal Approaches to Business Processes and Web Services (FABPWS'07)}, Editor = {Kees {van} Hee and Wolfgang Reisig and Karsten Wolf}, Month = jun, Pages = {21-35}, Publisher = {University of Podlasie}, Title = {A Feature-Complete {P}etri Net Semantics for {WS-BPEL 2.0}}, Year = 2007, Keywords = {oWFNs, BPEL-Semantik, BPEL, Services, Tools4BPEL}, Abstract = {We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification.} }Niels Lohmann, Peter Massuthe, and Karsten Wolf. Behavioral Constraints for Services. In Gustavo Alonso, Peter Dadam, and Michael Rosemann, editors, Business Process Management, 5th International Conference, BPM 2007, Brisbane, Australia, September 24-28, 2007, Proceedings, volume 4714 of Lecture Notes in Computer Science, pages 271-287, September 2007. Springer-Verlag.
Abstract: Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be "filtered" yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery. @inproceedings{LohmannMW2007_bpm, Author = {Niels Lohmann and Peter Massuthe and Karsten Wolf}, Booktitle = {Business Process Management, 5th International Conference, BPM 2007, Brisbane, Australia, September 24-28, 2007, Proceedings}, editor = {Gustavo Alonso and Peter Dadam and Michael Rosemann}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LohmannMW2007_bpm.pdf}, URL = {http://dx.doi.org/10.1007/978-3-540-75183-0_20}, Month = sep, Pages = {271-287}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Behavioral Constraints for Services}, Volume = {4714}, Year = {2007}, Abstract = {Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be "filtered" yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.} }Niels Lohmann, Peter Massuthe, and Karsten Wolf. Operating Guidelines for Finite-State Services. In Jetty Kleijn and Alex Yakovlev, editors, 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science, pages 321-341, 2007. Springer-Verlag.
Abstract: We study services modeled as open workflow nets (oWFN) and describe their behavior as service automata. Based on service automata, we introduce the concept of an operating guideline, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to properly interact (in this paper: deadlock-freely and with limited communication) with an oWFN N. It can be executed thus forming a properly interacting partner of N, or it can be used to support service discovery. An operating guideline for N is a particular service automaton S that is enriched with Boolean annotations. S interacts properly with the service automaton Prov, representing the behavior of N , and is able to simulate every other service that interacts properly with Prov . The attached annotations give complete information about whether or not a simulated service interacts properly with Prov, too. @inproceedings{LohmannMW2007_atpn, Author = {Niels Lohmann and Peter Massuthe and Karsten Wolf}, Booktitle = {28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 25-29, 2007, Proceedings}, Editor = {Jetty Kleijn and Alex Yakovlev}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Operating Guidelines for Finite-State Services}, Volume = {4546}, Pages = {321-341}, URL = {http://dx.doi.org/10.1007/978-3-540-73094-1_20}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LohmannMW2007_atpn.pdf}, Year = {2007}, Abstract = {We study services modeled as open workflow nets (oWFN) and describe their behavior as service automata. Based on service automata, we introduce the concept of an operating guideline, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to properly interact (in this paper: deadlock-freely and with limited communication) with an oWFN N. It can be executed thus forming a properly interacting partner of N, or it can be used to support service discovery. An operating guideline for N is a particular service automaton S that is enriched with Boolean annotations. S interacts properly with the service automaton Prov, representing the behavior of N , and is able to simulate every other service that interacts properly with Prov . The attached annotations give complete information about whether or not a simulated service interacts properly with Prov, too.} }Simon Moser, Axel Martens, Katharina Görlach, Wolfram Amme, and Artur Godlinski. Advanced Verification of Distributed WS-BPEL Business Processes Incorporating CSSA-based Data Flow Analysis. In IEEE International Conference on Services Computing (SCC 2007), pages 98-105, 2007.
Abstract: The Business Process Execution Language for Web Services WS-BPEL provides an technology to aggregate encapsulated functionalities for defining high-value Web services. For a distributed application in a B2B interaction, the partners simply need to expose their provided functionality as BPEL processes and compose them. Verifying such distributed web service based systems has been a huge topic in the research community lately - cf. [4] for a good overview. However, in most of the work on analyzing properties of interacting Web Services, especially when backed by stateful implementations like WS-BPEL, the data flow present in the implementation is widely neglected, and the analysis focusses on control flow only. This might lead to false-positive analysis results when searching for design weaknesses and errors, e.g. analyzing the controllability [14] of a given BPEL process. In this paper, we present a method to extract data flow information by constructing a CSSA representation and detecting data dependencies that effect communication behavior. Those discovered dependencies are used to construct a more precise formal model of the given BPEL process and hence to improve the quality of analysis results. @inproceedings{MoserMGAG2007_avdbp, author = {Simon Moser and Axel Martens and Katharina G{\"o}rlach and Wolfram Amme and Artur Godlinski}, title = {Advanced Verification of Distributed {WS-BPEL} Business Processes Incorporating {CSSA-based} Data Flow Analysis}, booktitle = {IEEE International Conference on Services Computing (SCC 2007)}, year = {2007}, pages = {98-105}, url = {http://doi.ieeecomputersociety.org/10.1109/SCC.2007.22}, abstract = {The Business Process Execution Language for Web Services WS-BPEL provides an technology to aggregate encapsulated functionalities for defining high-value Web services. For a distributed application in a B2B interaction, the partners simply need to expose their provided functionality as BPEL processes and compose them. Verifying such distributed web service based systems has been a huge topic in the research community lately - cf. [4] for a good overview. However, in most of the work on analyzing properties of interacting Web Services, especially when backed by stateful implementations like WS-BPEL, the data flow present in the implementation is widely neglected, and the analysis focusses on control flow only. This might lead to false-positive analysis results when searching for design weaknesses and errors, e.g. analyzing the controllability [14] of a given BPEL process. In this paper, we present a method to extract data flow information by constructing a CSSA representation and detecting data dependencies that effect communication behavior. Those discovered dependencies are used to construct a more precise formal model of the given BPEL process and hence to improve the quality of analysis results.} }Wolfgang Reisig, Jan Bretschneider, Dirk Fahland, Niels Lohmann, Peter Massuthe, and Christian Stahl. Services as a Paradigm of Computation. In Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjorner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007, volume 4700 of Lecture Notes in Computer Science, pages 521-538, September 2007. Springer-Verlag.
Abstract: The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques. @inproceedings{ReisigBFLMS2007_festschrift, Author = {Wolfgang Reisig and Jan Bretschneider and Dirk Fahland and Niels Lohmann and Peter Massuthe and Christian Stahl}, Title = {Services as a Paradigm of Computation}, Booktitle = {Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj{\o}rner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24-25, 2007}, Editor = {Cliff B. Jones and Zhiming Liu and Jim Woodcock}, Month = sep, Pages = {521-538}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Volume = {4700}, Year = {2007}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/ReisigBFLMS2007_festschrift.pdf}, URL = {http://dx.doi.org/10.1007/978-3-540-75221-9_25}, Abstract = {The recent success of service-oriented architectures gives rise to some fundamental questions: To what extent do services constitute a new paradigm of computation? What are the elementary ingredients of this paradigm? What are adequate notions of semantics, composition, equivalence? How can services be modeled and analyzed? This paper addresses and answers those questions, thus preparing the ground for forthcoming software design techniques.} }
Technische Berichte
Wil M. P. van der Aalst, Michael Beisiegel, Kees M. van Hee, Dieter König, and Christian Stahl. A SOA-Based Architecture Framework. Computer Science Report 07/02, Technische Universiteit Eindhoven, The Netherlands, January 2007.
Abstract: We present a SOA-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service Component Architecture (SCA). The framework is language independent and the building blocks of each system, activities and data, are first class citizens. We present a \emph{meta model} of the architecture framework and discuss its concepts in detail. Through the framework concepts such as wiring, correlation, and instantiation can be clarified. This allows us to demystify some of the confusion related to SOA. @TECHREPORT{AalstBHKS2007_csrep, AUTHOR = "{Wil} {M.} {P.} {van} {der} {Aalst} and Michael Beisiegel and {Kees} {M.} {van} Hee and Dieter K{\"o}nig and Christian Stahl", TITLE = "{A SOA-Based Architecture Framework}", INSTITUTION = "Technische Universiteit Eindhoven, The Netherlands", YEAR = "2007", type = "Computer Science Report", number = "07/02", month = "jan", keywords = "SOA, Architecture framework, SCA", abstract = {We present a SOA-based architecture framework. The architecture framework is designed to be close to industry standards, especially to the Service Component Architecture (SCA). The framework is language independent and the building blocks of each system, activities and data, are first class citizens. We present a \emph{meta model} of the architecture framework and discuss its concepts in detail. Through the framework concepts such as wiring, correlation, and instantiation can be clarified. This allows us to demystify some of the confusion related to SOA.}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/AalstBHKS2007_csrep.pdf} }Wil M. P. van der Aalst, Peter Massuthe, Arjan J. Mooij, Christian Stahl, and Karsten Wolf. Erratum -- Multiparty Contracts: Agreeing and Implementing Interorganizational Processes. Informatik-Berichte 213, Humboldt-Universität zu Berlin, June 2007.
@TECHREPORT{AalstMSW2007_hub_tr213-erratum, Author = {{Wil} {M.} {P.} {van} {der} {Aalst} and Peter Massuthe and Arjan J. Mooij and Christian Stahl and Karsten Wolf}, Institution = {Humboldt-Universit{\"a}t zu Berlin}, Number = {213}, Title = {{Erratum -- Multiparty Contracts: Agreeing and Implementing Interorganizational Processes}}, Type = {Informatik-Berichte}, Year = {2007}, Month = jun, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/AalstMSW2007_hub_tr213-erratum.pdf}, keywords = {oWFNs, Services, Operating Guidelines} }Wil M. P. van der Aalst, Peter Massuthe, Christian Stahl, and Karsten Wolf. Multiparty Contracts: Agreeing and Implementing Interorganizational Processes. Informatik-Berichte 213, Humboldt-Universität zu Berlin, June 2007. Note: There is an erratum.
Abstract: A contract specifies an interorganizational process together with a distribution of responsibilities for the activities among the parties involved. In this paper, we formally show how a party can implement its part of the contract such that the implementation accords with the contract. We propose a formal notion of a contract and give a criterion for accordance between a local implementation and a contract such that, if all local implementations accord with the contract, the overall process is deadlock-free and it is always possible to terminate properly. Then, we sketch a technique for automatically checking the proposed accordance criterion. Finally, we present accordance-preserving transformation rules. These rules can be used to implement a part of the contract while preserving the accordance criterion. @TECHREPORT{AalstMSW2007_hub_tr213, Author = {{Wil} {M.} {P.} {van} {der} {Aalst} and Peter Massuthe and Christian Stahl and Karsten Wolf}, Institution = {Humboldt-Universit{\"a}t zu Berlin}, Number = {213}, Title = {{Multiparty Contracts: Agreeing and Implementing Interorganizational Processes}}, Type = {Informatik-Berichte}, Year = {2007}, Month = jun, note = {there is an erratum}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/AalstMSW2007_hub_tr213.pdf}, abstract = {A contract specifies an interorganizational process together with a distribution of responsibilities for the activities among the parties involved. In this paper, we formally show how a party can implement its part of the contract such that the implementation accords with the contract. We propose a formal notion of a contract and give a criterion for accordance between a local implementation and a contract such that, if all local implementations accord with the contract, the overall process is deadlock-free and it is always possible to terminate properly. Then, we sketch a technique for automatically checking the proposed accordance criterion. Finally, we present accordance-preserving transformation rules. These rules can be used to implement a part of the contract while preserving the accordance criterion.}, keywords = {oWFNs, Services, Operating Guidelines, Exchangeability} }Kees M. van Hee, Natalia Sidorova, Christian Stahl, and H. M. W. Verbeek. A Price of Service in a Compositional SOA Framework. Computer Science Report 07/16, Technische Universiteit Eindhoven, The Netherlands, July 2007.
Abstract: In this paper we propose a framework for SOA covering such important features as proper termination (soundness) and correct correlation of tasks. Within this framework, we define a method for the calculation of the price of services. Our framework is compositional in the sense that composing a system from subsystems that meet our correctness requirements we obtain a system that still meets these requirements. @TECHREPORT{HeeSSV2007_csrep, AUTHOR = "{Kees} {M.} {van} {Hee} and Natalia Sidorova and Christian Stahl and {H.} {M.} {W.} Verbeek", TITLE = "{A Price of Service in a Compositional SOA Framework}", INSTITUTION = "Technische Universiteit Eindhoven, The Netherlands", YEAR = "2007", type = "Computer Science Report", number = "07/16", month = "jul", keywords = "SOA, Architecture framework", abstract = {In this paper we propose a framework for SOA covering such important features as proper termination (soundness) and correct correlation of tasks. Within this framework, we define a method for the calculation of the price of services. Our framework is compositional in the sense that composing a system from subsystems that meet our correctness requirements we obtain a system that still meets these requirements.}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/HeeSSV2007_csrep.pdf}, url = {http://library.tue.nl/catalog/FullBB.csp?ExtraInfo=&SearchTerm1=***N.6.631702&SearchT1=&Index1=Index1&ItemNr=8&Database=6&SearchMethod=Find_1&OpacLanguage=eng&Profile=Default&RequestId=192856_3&PageType=FullBB&PreviousList=FullBB&NumberToRetrieve=50&WebAction=ShowFullBB&RecordNumber=1&StartValue=1&SaveListInfo=General_192856_Dummy} }Bodo Hohberg, Wolfgang Reisig, and Bixia Wu. Entwurf und Verifikation nachrichtenbasierter verteilter Algorithmen durch verteilende Verfeinerung. Informatik-Berichte 216, Humboldt-Universität zu Berlin, 2007.
Abstract: Um Entwurf und Verifikation komplizierter verteilter Algorithmen leichter und verständlicher zu machen, wird oft eine Verfeinerungsmethode verwendet. Dabei wird ein einfacher Algorithmus, der gewünschte Eigenschaften erfüllt, schrittweise zu einem komplizierten Algorithmus verfeinert. In jedem Schritt sollen die gewünschten Eigenschaften erhalten bleiben. Für nachrichtenbasierte verteilte Algorithmen, die durch Petrinetze modelliert werden, haben wir eine neue Verfeinerungsmethmode entwickelt. Wir beginnen mit einem Anfangsalgorithmus, der Aktionen enthält, die gemeinsame Aufgaben mehrerer Agenten beschreiben. In jedem Schritt verfeinern wir eine dieser Aktionen zu einem Netz, das nur solche Aktionen enthält, die die Aufgaben einzelner Agenten beschreiben. Jeder Schritt ist also eine Verteilung einer unverteilten Aktion, also eine verteilende Verfeinerung. Die Arbeit klärt den Zusammenhang von Eigenschaften des Verfeinerungsnetzes und den bei der Verfeinerung gültig bleibenden Eigenschaften des verfeinerten Algorithmus. Hierbei sind Kausalitäten im Verfeinerungsnetz von entscheidender Bedeutung. Die Anwendung der Methode wird in der Arbeit an anschaulichen Beispielen demonstriert. @TechReport{HohbergRW2007_hub_tr216, author = {Bodo Hohberg and Wolfgang Reisig and Bixia Wu}, title = {Entwurf und Verifikation nachrichtenbasierter verteilter Algorithmen durch verteilende Verfeinerung}, institution = {Humboldt-Universit{\"{a}}t zu Berlin}, year = 2007, type = {Informatik-Berichte}, number = 216, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/HohbergRW2007_hub_tr216.pdf}, abstract = {Um Entwurf und Verifikation komplizierter verteilter Algorithmen leichter und verständlicher zu machen, wird oft eine Verfeinerungsmethode verwendet. Dabei wird ein einfacher Algorithmus, der gewünschte Eigenschaften erfüllt, schrittweise zu einem komplizierten Algorithmus verfeinert. In jedem Schritt sollen die gewünschten Eigenschaften erhalten bleiben. Für nachrichtenbasierte verteilte Algorithmen, die durch Petrinetze modelliert werden, haben wir eine neue Verfeinerungsmethmode entwickelt. Wir beginnen mit einem Anfangsalgorithmus, der Aktionen enthält, die gemeinsame Aufgaben mehrerer Agenten beschreiben. In jedem Schritt verfeinern wir eine dieser Aktionen zu einem Netz, das nur solche Aktionen enthält, die die Aufgaben einzelner Agenten beschreiben. Jeder Schritt ist also eine Verteilung einer unverteilten Aktion, also eine verteilende Verfeinerung. Die Arbeit klärt den Zusammenhang von Eigenschaften des Verfeinerungsnetzes und den bei der Verfeinerung gültig bleibenden Eigenschaften des verfeinerten Algorithmus. Hierbei sind Kausalitäten im Verfeinerungsnetz von entscheidender Bedeutung. Die Anwendung der Methode wird in der Arbeit an anschaulichen Beispielen demonstriert.} }Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, and Karsten Wolf. Extending the Compatibility Notion for Abstract WS-BPEL Processes. Preprint CS-02-07, Universität Rostock, Rostock, Germany, November 2007.
Abstract: WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible. @techreport{KoenigLMSW2007_tr_cs0207, Address = {Rostock, Germany}, Author = {Dieter K{\"o}nig and Niels Lohmann and Simon Moser and Christian Stahl and Karsten Wolf}, Institution = {Universit{\"a}t Rostock}, Month = nov, Number = {CS-02-07}, Title = {Extending the Compatibility Notion for Abstract {WS-BPEL} Processes}, Type = {Preprint}, Year = {2007}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/KoenigLMSW2007_tr_cs0207.pdf}, Abstract = {WS-BPEL defines a standard for executable business processes. Executable processes are business processes which can be automated through an IT infrastructure. The WS-BPEL specification also introduces the concept of abstract processes: In contrast to their executable siblings, abstract processes are not executable and can have parts where business logic is disguised. Nevertheless, the WS-BPEL specification introduces a notion of compatibility between such an under-specified abstract process and a fully specified executable one. Basically, this compatibility notion defines a set of syntactical rules that can be augmented or restricted by profiles. So far, there exists two of such profiles: the Abstract Process Profile for Observable Behavior and the Abstract Process Profile for Templates. None of these profiles defines a concept of behavioral equivalence. Therefore, both profiles are too strict with respect to the rules they impose when deciding whether an executable process is compatible to an abstract one. In this paper, we propose a novel profile that extends the existing Abstract Process Profile for Observable Behavior by defining a behavioral relationship. We also show that our novel profile allows for more flexibility when deciding whether an executable and an abstract process are compatible.} }Niels Lohmann. A Feature-Complete Petri Net Semantics for WS-BPEL 2.0 and its Compiler BPEL2oWFN. Informatik-Berichte 212, Humboldt-Universität zu Berlin, August 2007.
Abstract: We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification. This technical report is the extended version of the papers [1, 2] and can be seen as the sequel of [3]. @TechReport{Lohmann2007_hub_tr212, author = {Niels Lohmann}, title = {A Feature-Complete {P}etri Net Semantics for {WS-BPEL} 2.0 and its Compiler {BPEL2oWFN}}, institution = {Humboldt-Universit{\"{a}}t zu Berlin}, year = 2007, type = {Informatik-Berichte}, number = 212, month = aug, keywords = {BPEL, BPEL-Semantik, Tools4BPEL}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Lohmann2007_hub_tr212.pdf}, abstract = {We present an extension of a Petri net semantics for the Web Service Business Execution Language (WS-BPEL). This extension covers the novel activities and constructs introduced by the recent WS-BPEL 2.0 specification. Furthermore, we simplify several aspects of the Petri net semantics to allow for more compact models suited for computer-aided verification. This technical report is the extended version of the papers [1, 2] and can be seen as the sequel of [3].} }Niels Lohmann, Peter Massuthe, and Karsten Wolf. Behavioral Constraints for Services. Informatik-Berichte 214, Humboldt-Universität zu Berlin, May 2007.
Abstract: Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be ``filtered'' yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery. @TechReport{ LohmannMW2007_hub_tr214, author = {Niels Lohmann and Peter Massuthe and Karsten Wolf}, title = {Behavioral Constraints for Services}, institution = {Humboldt-Universit{\"{a}}t zu Berlin}, year = 2007, type = {Informatik-Berichte}, number = 214, month = may, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LohmannMW2007_hub_tr214.pdf}, abstract = {Recently, we introduced the concept of an operating guideline of a service as a structure that characterizes all its properly interacting partner services. The hitherto considered correctness criterion is deadlock freedom of the composition of both services. In practice, there are intended and unintended deadlock-freely interacting partners of a service. In this paper, we provide a formal approach to express intended and unintended behavior as behavioral constraints. With such a constraint, unintended partners can be ``filtered'' yielding a customized operating guideline. Customized operating guidelines can be applied to validate a service and for service discovery.} }Niels Lohmann, H. M. W. Verbeek, Chun Ouyang, Christian Stahl, and Wil M. P. van der Aalst. Comparing and Evaluating Petri Net Semantics for BPEL. Computer Science Report 07/23, Technische Universiteit Eindhoven, The Netherlands, August 2007.
Abstract: We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modeling decisions. These decisions together with their consequences are discussed.We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model. @techreport{LohmannVOSA2007_techreport, Author = {Niels Lohmann and {H.} {M.} {W.} Verbeek and Chun Ouyang and Christian Stahl and {Wil} {M.} {P.} {van} {der} {Aalst}}, Institution = {Technische Universiteit Eindhoven, The Netherlands}, Month = aug, Number = {07/23}, Title = {Comparing and Evaluating {Petri} Net Semantics for {BPEL}}, Type = {Computer Science Report}, Year = {2007}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/LohmannVOSA2007_techreport.pdf}, Abstract = {We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modeling decisions. These decisions together with their consequences are discussed.We also give an overview of the different properties that can be verified on the resulting models. A case study helps to evaluate the corresponding compilers which transform a BPEL process into a Petri net model.}, url = {http://library.tue.nl/catalog/FullBB.csp?Profile=Default&OpacLanguage=dut&SearchMethod=Find_1&PageType=Start&PreviousList=Start&NumberToRetrieve=10&RecordNumber=&WebPageNr=1&StartValue=1&Database=6&Index1=Index1&RequestId=924366_1&WebAction=ShowFullBB&SearchT1=.6.630637&SearchTerm1=.6.630637&OutsideLink=Yes&ShowMenu=Yes} }
Studien- und Diplomarbeiten
Jan Bretschneider. Produktbedienungsanleitungen zur Charakterisierung austauschbarer Services. Diplomarbeit, Humboldt-Universität zu Berlin, March 2007.
Abstract: Unternehmen sind bestrebt, immer mehr Geschäfte mit ihren Kunden teilweise oder vollständig automatisiert abzuwickeln. In diesem Bestreben machen sie mehr und mehr Gebrauch von der serviceorientierten Architektur (SOA). Grundbaustein der SOA ist der Service, der eine von einem Unternehmen angebotene Dienstleistung oder Funktionalität über eine wohldefinierte Schnittstelle bereitstellt und von Kunden oder Services anderer Unternehmen verwendet werden kann. Damit wir zwei Services als sinnvoll miteinander interagierend bezeichnen können, müssen sie verschiedene Mindestanforderungen erfüllen. Auf Grundlage dieser Mindestanforderungen können wir für jeden gegebenen Service eine Bedienungsanleitung konstruieren, die alle sinnvoll mit ihm interagierenden Services charakterisiert. Auch tritt die Frage auf, gegen welche Services ein Service ausgetauscht werden kann, so dass alle Services, die mit dem alten sinnvoll interagieren konnten, auch mit dem neuen sinnvoll interagieren können. Diesen allgemeinen Austauschbarkeitsbegriff parametrisieren wir in der vorliegenden Arbeit und beschäftigen uns mit dem Fall, dass durch den Austausch eines Services nur eine bestimmte Menge von Services unberührt bleiben soll, weil dies eine größere Freiheit in der Wahl des austauschenden Service erlaubt. Wir werden die Menge der Services, gegen die sich ein bestimmter Service bezüglich einer gegebenen Menge von Services austauschen lässt, mit Hilfe des Konzepts der Bedienungsanleitungen genau charakterisieren. @MastersThesis{Bretschneider2007_da, author = {Jan Bretschneider}, title = {{Produktbedienungsanleitungen zur Charakterisierung austauschbarer Services}}, school = {Humboldt-Universität zu Berlin}, year = 2007, type = {Diplomarbeit}, month = mar, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Bretschneider2007_da.pdf}, keywords = {Operating Guidelines}, abstract={Unternehmen sind bestrebt, immer mehr Geschäfte mit ihren Kunden teilweise oder vollständig automatisiert abzuwickeln. In diesem Bestreben machen sie mehr und mehr Gebrauch von der serviceorientierten Architektur (SOA). Grundbaustein der SOA ist der Service, der eine von einem Unternehmen angebotene Dienstleistung oder Funktionalität über eine wohldefinierte Schnittstelle bereitstellt und von Kunden oder Services anderer Unternehmen verwendet werden kann. Damit wir zwei Services als sinnvoll miteinander interagierend bezeichnen können, müssen sie verschiedene Mindestanforderungen erfüllen. Auf Grundlage dieser Mindestanforderungen können wir für jeden gegebenen Service eine Bedienungsanleitung konstruieren, die alle sinnvoll mit ihm interagierenden Services charakterisiert. Auch tritt die Frage auf, gegen welche Services ein Service ausgetauscht werden kann, so dass alle Services, die mit dem alten sinnvoll interagieren konnten, auch mit dem neuen sinnvoll interagieren können. Diesen allgemeinen Austauschbarkeitsbegriff parametrisieren wir in der vorliegenden Arbeit und beschäftigen uns mit dem Fall, dass durch den Austausch eines Services nur eine bestimmte Menge von Services unberührt bleiben soll, weil dies eine größere Freiheit in der Wahl des austauschenden Service erlaubt. Wir werden die Menge der Services, gegen die sich ein bestimmter Service bezüglich einer gegebenen Menge von Services austauschen lässt, mit Hilfe des Konzepts der Bedienungsanleitungen genau charakterisieren.} }Christian Gierds. Ein schärferes Kriterium für die Wahl von Endzuständen in Bedienungsanleitungen, Liberalsten Partnern und Public Views. Studienarbeit, Humboldt-Universität zu Berlin, October 2007.
Abstract: In der Welt der Service Orientierten Architektur (SOA) besteht der Bedarf, Dienste auf ihre mögliche Interaktion mit anderen Diensten hin zu untersuchen. Dienste werden wir in Form von Serviceautomaten betrachten, die als asynchron kommunizierende Automaten definiert sind. Um die Frage einer sinnvollen, also verklemmungsfreien Kommunikation zu klären, gibt es das Konzept der Bedienungsanleitungen. Wie werden für diese ein scharfes Kriterium für die Wahl der Endzustände angeben und zeigen, dass diese Wahl sich in vorhandene Konzepte integriert. Besonderes Augenmerk werden wir dabei auf den Liberalsten Partner und den Public View eines Serviceautomaten werfen und an diesen unsere Definition rechtfertigen. @MastersThesis{Gierds2007_sa, author = {Christian Gierds}, title = {{Ein schärferes Kriterium für die Wahl von Endzuständen in Bedienungsanleitungen, Liberalsten Partnern und Public Views}}, school = {Humboldt-Universität zu Berlin}, year = 2007, type = {Studienarbeit}, month = oct, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Gierds2007_sa.pdf}, keywords = {Services, oWFNs, Bedienbarkeit, Endzustände}, abstract = {In der Welt der Service Orientierten Architektur (SOA) besteht der Bedarf, Dienste auf ihre mögliche Interaktion mit anderen Diensten hin zu untersuchen. Dienste werden wir in Form von Serviceautomaten betrachten, die als asynchron kommunizierende Automaten definiert sind. Um die Frage einer sinnvollen, also verklemmungsfreien Kommunikation zu klären, gibt es das Konzept der Bedienungsanleitungen. Wie werden für diese ein scharfes Kriterium für die Wahl der Endzustände angeben und zeigen, dass diese Wahl sich in vorhandene Konzepte integriert. Besonderes Augenmerk werden wir dabei auf den Liberalsten Partner und den Public View eines Serviceautomaten werfen und an diesen unsere Definition rechtfertigen.} }Alexandra Julius. Abstrakte Datenflussmodelle für GALS-Schaltungen zum Nachweis nicht-funktionaler Eigenschaften. Diplomarbeit, Humboldt-Universität zu Berlin, May 2007.
Abstract: In dieser Arbeit stellen wir Möglichkeiten vor, nicht-funktionale Eigenschaften einer GALS-Schaltung mittels Modellierung, Abstraktion und Verifikation zu analysieren. Im Mittelpunkt der Untersuchungen steht vor allem das Zeitverhalten und die Funktionssicherheit der Schaltung. Mit geeigneten Datenflussmodellen, in denen Zeit explizit modelliert ist, werden diese Eigenschaften untersucht. Da die Modellierung von Zeit die Komplexität des Modells erhöht und damit auch die Verikation erschwert, modellieren wir den Datenfluss möglichst abstrakt. Wir schlagen in dieser Arbeit mehrere Abstraktionstechniken vor, die den Zustandsraum des Datenmodells reduzieren. @MastersThesis{Julius2007_da, author = {Alexandra Julius}, title = {{Abstrakte Datenflussmodelle für GALS-Schaltungen zum Nachweis nicht-funktionaler Eigenschaften}}, school = {Humboldt-Universität zu Berlin}, year = 2007, type = {Diplomarbeit}, month = may, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Diplomarbeit-Julius.pdf}, keywords = {GALS}, abstract = {In dieser Arbeit stellen wir Möglichkeiten vor, nicht-funktionale Eigenschaften einer GALS-Schaltung mittels Modellierung, Abstraktion und Verifikation zu analysieren. Im Mittelpunkt der Untersuchungen steht vor allem das Zeitverhalten und die Funktionssicherheit der Schaltung. Mit geeigneten Datenflussmodellen, in denen Zeit explizit modelliert ist, werden diese Eigenschaften untersucht. Da die Modellierung von Zeit die Komplexität des Modells erhöht und damit auch die Verikation erschwert, modellieren wir den Datenfluss möglichst abstrakt. Wir schlagen in dieser Arbeit mehrere Abstraktionstechniken vor, die den Zustandsraum des Datenmodells reduzieren.} }Andreas Kerlin. Bedienbarkeit unter Kausalität. Diplomarbeit, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, January 2007.
@MastersThesis{Kerlin2007_da, author = {Andreas Kerlin}, title = {{Bedienbarkeit unter Kausalität}}, school = {Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II}, year = {2007}, type = {Diplomarbeit}, month = {jan}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Kerlin2007_da.pdf} }Jens Kleine. Transformation von offenen Workflow-Netzen zu abstrakten WS-BPEL-Prozessen. Diplomarbeit, Humboldt-Universität zu Berlin, July 2007.
Abstract: In dieser Arbeit präsentieren wir eine Transformation von offenenWorkflow-Netzen zu abstrakten WS-BPEL-Prozessen. Als Web Services implementierte Geschäftsprozesse sind zunehmend verbreiteter und von größerer finanzieller Bedeutung. Daher müssen sie vor ihrem Einsatz auf wichtige Eigenschaften wie korrekte Terminierung oder Bedienbarkeit überprüft werden. Die häufig eingesetzte Modellierungssprache WS-BPEL ist jedoch auf Grund ihrer fehlenden formalen Semantik nicht analysierbar. Aus diesem Grund existieren Werkzeuge zur Überführung von WS-BPEL-Prozessen in die Petrinetzklasse der offenen Workflow-Netze. Für diese kann auf eine Reihe von Tools zur formalen Analyse von Geschäftsprozessen zurückgegriffen werden. Unsere Transformation ermöglicht es, die Ergebnisse dieser Analysewerkzeuge vollautomatisch in WS-BPEL-Prozesse zurück zu übersetzen. So können unter anderem Beispiele für im Prozess auftretende Fehler und bedienende Partner als WS-BPEL-Code an den Anwender zurückgegeben werden, ohne dass dieser sich dazu mit den, in den Zwischenschritten der Analyse verwendeten, Petrinetzen auskennen muss. Zudem bietet unsere Transformation die Möglichkeit Geschäftsprozesse graphbasiert als offene Workflow-Netze zu modellieren und diese anschließend automatisch in einen abstrakten WS-BPEL-Prozess zu übersetzen. @MastersThesis{Kleine2007_da, author = {Jens Kleine}, title = {{Transformation von offenen Workflow-Netzen zu abstrakten WS-BPEL-Prozessen}}, school = {Humboldt-Universität zu Berlin}, year = 2007, type = {Diplomarbeit}, month = jul, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Kleine2007_da.pdf}, abstract = {In dieser Arbeit präsentieren wir eine Transformation von offenenWorkflow-Netzen zu abstrakten WS-BPEL-Prozessen. Als Web Services implementierte Geschäftsprozesse sind zunehmend verbreiteter und von größerer finanzieller Bedeutung. Daher müssen sie vor ihrem Einsatz auf wichtige Eigenschaften wie korrekte Terminierung oder Bedienbarkeit überprüft werden. Die häufig eingesetzte Modellierungssprache WS-BPEL ist jedoch auf Grund ihrer fehlenden formalen Semantik nicht analysierbar. Aus diesem Grund existieren Werkzeuge zur Überführung von WS-BPEL-Prozessen in die Petrinetzklasse der offenen Workflow-Netze. Für diese kann auf eine Reihe von Tools zur formalen Analyse von Geschäftsprozessen zurückgegriffen werden. Unsere Transformation ermöglicht es, die Ergebnisse dieser Analysewerkzeuge vollautomatisch in WS-BPEL-Prozesse zurück zu übersetzen. So können unter anderem Beispiele für im Prozess auftretende Fehler und bedienende Partner als WS-BPEL-Code an den Anwender zurückgegeben werden, ohne dass dieser sich dazu mit den, in den Zwischenschritten der Analyse verwendeten, Petrinetzen auskennen muss. Zudem bietet unsere Transformation die Möglichkeit Geschäftsprozesse graphbasiert als offene Workflow-Netze zu modellieren und diese anschließend automatisch in einen abstrakten WS-BPEL-Prozess zu übersetzen.} }Peter Laufer. Public-View-Generierung. Diplomarbeit, Humboldt-Universität zu Berlin, November 2007.
Abstract: Die Analyse und Optimierung der Geschäftsprozesse ist von enormer Bedeutung für den langfristigen Erfolg eines Unternehmens. Die Märkte sind heutzutage zunehmend global und befinden sich in stetem Wandel, was eine fortwährende Überprüfung und Anpassung der Prozesse innerhalb eines Unternehmens erfordert. Durch den rasanten technologischen Fortschritt und den vermehrten Einsatz von Computern lassen sich immer größere Teile von Prozessen automatisieren. Einen neuen Ansatz zur Realisierung der IT-Infrastruktur in Unternehmen stellt dabei die service-orientierte Architektur (SOA) dar. Services, die eine wohldefinierte Funktionalität in einem Netzwerk zur Verfügung stellen, lassen sich unter relativ geringem Aufwand zu neuen Prozessen kombinieren und bei Bedarf ersetzen, ohne dass eine kostenintensive Anpassung vorhandener Lösungen erforderlich ist. Über das Internet können Dienste als sog. Web-Services zur Verfügung gestellt werden und so in die Abläufe der Prozesse anderer Unternehmen integriert werden. Um Services für potentielle Interessenten bekannt zu machen, muss eine Beschreibung der Funktionalität bei einem Verzeichnisdienst (service broker) hinterlegt werden. Im Bereich der Veröffentlichung von Services in Verzeichnisdiensten bieten sich zwei Konzepte zur Abstraktion von unternehmensinternen Informationen der Prozesse an: der Public View und die Bedienungsanleitung. Während für beliebige Prozesse eine Bedienungsanleitung automatisch berechnet werden kann und es Algorithmen gibt, die auf Basis der Bedienungsanleitungen entscheiden können, ob zwei Prozesse problemlos miteinander interagieren können, muss ein Public View bisher noch von einem Entwickler per Hand modelliert werden. Eine solche Modellierung ist jedoch aufwendig, fehleranfällig und kann ohne eine anschließende Verifikation nicht garantieren, dass sich der ursprüngliche Prozess P und sein Public View P' in Bezug auf die Bedienbarkeit äquivalent verhalten. Wir wollen uns in dieser Arbeit daher mit Verfahren zur automatischen Public-View-Generierung befassen. Verschiedene Ansätze werden im Detail vorgestellt und miteinander verglichen. Anhand von Fallstudien werden wir die Stärken und Schwächen der Verfahren näher beleuchten und Empfehlungen zu deren Einsatz ableiten. @MastersThesis{Laufer2007_da, author = {Peter Laufer}, title = {{Public-View-Generierung}}, school = {Humboldt-Universität zu Berlin}, year = 2007, type = {Diplomarbeit}, month = nov, keywords = {SOA, Services, Operating Guidelines}, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Laufer2007_da.pdf}, abstract={Die Analyse und Optimierung der Geschäftsprozesse ist von enormer Bedeutung für den langfristigen Erfolg eines Unternehmens. Die Märkte sind heutzutage zunehmend global und befinden sich in stetem Wandel, was eine fortwährende Überprüfung und Anpassung der Prozesse innerhalb eines Unternehmens erfordert. Durch den rasanten technologischen Fortschritt und den vermehrten Einsatz von Computern lassen sich immer größere Teile von Prozessen automatisieren. Einen neuen Ansatz zur Realisierung der IT-Infrastruktur in Unternehmen stellt dabei die service-orientierte Architektur (SOA) dar. Services, die eine wohldefinierte Funktionalität in einem Netzwerk zur Verfügung stellen, lassen sich unter relativ geringem Aufwand zu neuen Prozessen kombinieren und bei Bedarf ersetzen, ohne dass eine kostenintensive Anpassung vorhandener Lösungen erforderlich ist. Über das Internet können Dienste als sog. Web-Services zur Verfügung gestellt werden und so in die Abläufe der Prozesse anderer Unternehmen integriert werden. Um Services für potentielle Interessenten bekannt zu machen, muss eine Beschreibung der Funktionalität bei einem Verzeichnisdienst (service broker) hinterlegt werden. Im Bereich der Veröffentlichung von Services in Verzeichnisdiensten bieten sich zwei Konzepte zur Abstraktion von unternehmensinternen Informationen der Prozesse an: der Public View und die Bedienungsanleitung. Während für beliebige Prozesse eine Bedienungsanleitung automatisch berechnet werden kann und es Algorithmen gibt, die auf Basis der Bedienungsanleitungen entscheiden können, ob zwei Prozesse problemlos miteinander interagieren können, muss ein Public View bisher noch von einem Entwickler per Hand modelliert werden. Eine solche Modellierung ist jedoch aufwendig, fehleranfällig und kann ohne eine anschließende Verifikation nicht garantieren, dass sich der ursprüngliche Prozess P und sein Public View P' in Bezug auf die Bedienbarkeit äquivalent verhalten. Wir wollen uns in dieser Arbeit daher mit Verfahren zur automatischen Public-View-Generierung befassen. Verschiedene Ansätze werden im Detail vorgestellt und miteinander verglichen. Anhand von Fallstudien werden wir die Stärken und Schwächen der Verfahren näher beleuchten und Empfehlungen zu deren Einsatz ableiten.} }Nannette Liske. Laufzeitersetzbarkeit von Services. Studienarbeit, Humboldt-Universität zu Berlin, April 2007.
@MastersThesis{Liske2007_sa, author = {Nannette Liske}, title = {{Laufzeitersetzbarkeit von Services}}, school = {Humboldt-Universität zu Berlin}, year = 2007, type = {Studienarbeit}, month = apr, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Liske2007_sa.pdf} }Gerrit Müller. Strukturelle Analyse von offenen Workflow-Netzen hinsichtlich Bedienbarkeit. Studienarbeit, Humboldt-Universität zu Berlin, January 2007.
@MastersThesis{Mueller2007_sa, author = {Gerrit Müller}, title = {{Strukturelle Analyse von offenen Workflow-Netzen hinsichtlich Bedienbarkeit}}, school = {Humboldt-Universität zu Berlin}, year = 2007, type = {Studienarbeit}, month = jan, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Mueller2007_sa.pdf}, keywords = {oWFNs, Bedienbarkeit, Interaktionsgraph}, abstract = {} }Alexander Schulz. Zielgerichtete Strategien. Studienarbeit, Humboldt-Universität zu Berlin, July 2007.
@MastersThesis{Schulz2007_sa, author = {Alexander Schulz}, title = {{Zielgerichtete Strategien}}, school = {Humboldt-Universität zu Berlin}, year = 2007, type = {Studienarbeit}, month = jul, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Schulz2007_sa.pdf}, keywords = {Services, oWFNs, Bedienbarkeit}, abstract = {} }Manja Wolf. Synchrone und asynchrone Kommunikation in offenen Workflownetzen. Studienarbeit, Humboldt-Universität zu Berlin, May 2007.
@MastersThesis{Wolf2007_sa, author = {Manja Wolf}, title = {{Synchrone und asynchrone Kommunikation in offenen Workflownetzen}}, school = {Humboldt-Universität zu Berlin}, year = 2007, type = {Studienarbeit}, month = may, pdf = {http://www.informatik.hu-berlin.de/top/download/publications/Wolf2007_sa.pdf} }
Theorie der Programmierung | | XHTML 1.0 | Wed Nov 5 08:30:01 2008

