Publikationen zum Fachbereich Services

Dissertationen und Habilitationen

Peter Massuthe. Operating Guidelines for Services. Dissertation, Humboldt-Universit�t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult�t II; Eindhoven University of Technology, April 2009. Note: ISBN 978-90-386-1702-2.

Christian Stahl. Service Substitution - A Behavioral Approach Based on Petri Nets. Dissertation, Humboldt-Universit�t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult�t II; Eindhoven University of Technology, December 2009. Note: ISBN 978-90-386-2065-7.

Abstract: Service-Oriented Computing is an emerging computing paradigm that supports the modular design of (software) systems. Complex systems are designed by composing less complex systems, called services. Such a (complex) system is a distributed application often involving several cooperating enterprises. As a system usually changes over time, individual services will be substituted by other services. Substituting one service by another one should not affect the correctness of the overall system. Assuring correctness becomes particularly challenging, as the services rely on each other, and each of the involved enterprises only oversees a part of the overall system. In addition, services communicate asynchronously which makes the analysis even more difficult. For this reason, formal methods to support service substitution are indispensable. In this thesis, we study service substitution at the level of service models. Thereby we restrict ourselves to service behavior. As a formalism to model service behavior, we use Petri nets. The first contribution of this thesis is the definition of several substitutability criteria that are suitable in the context of Service-Oriented Computing. Substituting a service S by a service S' should preserve some behavioral properties of the overall system. For each set of behavioral properties and a given service S, there exists a set of behaviorally compatible services for S. A substitutability criterion defines which of these behaviorally compatible services of S have to be preserved by S'. We relate our substitutability criteria to preorders and equivalences known from process theory. The second contribution of this thesis is to present, for each substitutability criterion, a procedure to decide whether a service S' can substitute a service S. The decision requires the comparison of the in general infinite sets of behaviorally compatible services for the services S and S'. Hence, we extend existing work on an abstract representation of all behaviorally compatible services for a given service. For each notion of behavioral compatibility, we present an algorithmic solution to represent all behaviorally compatible services. Based on these representations, we can decide substitutability of a service S by a service S'. The third contribution of this thesis is a method to support the design of a service S' that can substitute a service $S$ according to a substitutability criterion. Our approach is to derive a service S' from the service S by stepwise transformation. To this end, we present several transformation rules. Finally, we formalize and we extend the equivalence notion for services specified in the language WS-BPEL. That way, we demonstrate the applicability of our work.

Axel Martens. Verteilte Gesch�ftsprozesse - Modellierung und Verifikation mit Hilfe von Web Services. Dissertation, Humboldt-Universit�t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult�t II, 2003. Note: Erschienen in WiKi: Stuttgart, Berlin & Paris.

Publikationen in Zeitschriften und B�chern

Arjan J. Mooij, Christian Stahl, and Marc Voorhoeve. Relating Fair Testing and Accordance for Service Replaceability. Journal of Logic and Algebraic Programming, 2010. Note: To appear.

Abstract: The accordance pre-order describes whether a service can safely be replaced by another service. That is, all partners for the original service should be partners for the new service. Partners for a service interact with the service in such a way that always a certain common goal can be reached. We relate the accordance pre-order to the pre-orders known from the linear-branching time spectrum, notably fair testing. The differences between accordance and fair testing include the modeling of termination and success, and the parts of the services that cannot be used reliably by any partner. Apart from the theoretical results, we address the practical relevance of the introduced concepts.

Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, and Karsten Wolf. Multiparty Contracts: Agreeing and Implementing Interorganizational Processes. The Computer Journal, 53(1): 90-106, 2010.

Abstract: To implement an interorganizational process between different enterprizes, one needs to agree on the ``rules of engagement''. These can be specified in terms of a contract that describes the overall intended process and the duties of all parties involved. We propose to use such a process-oriented contract which can be seen as the composition of the public views of all participating parties. Based on this contract each party may locally implement its part of the contract such that the implementation (the private view) agrees on the contract. In this paper, we propose a formal notion for such process-oriented contracts and give a criterion for accordance between a private view and its public view. The public view of a party can be substituted by a private view if and only if the private view accords with the public view. Using the notion of accordance the overall implemented process is guaranteed to be deadlock-free and it is always possible to terminate properly. In addition, we present a technique for automatically checking our accordance criterion. A case study illustrates how our proposed approach can be used in practice.

Niels Lohmann, Eric Verbeek, Chun Ouyang, and Christian Stahl. Comparing and Evaluating Petri Net Semantics for BPEL. International Journal of Business Process Integration and Management (IJBPIM), 4(1): 60-73, 2009.

Abstract: We compare two Petri net semantics for the Web Services Business Process Execution Language (BPEL). The comparison reveals different modelling 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.

Christian Stahl, Peter Massuthe, and Jan Bretschneider. Deciding Substitutability of Services with Operating Guidelines. Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems, 2(5460): 172-191, March 2009.

Abstract: Deciding whether a service S can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of restriction can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.

Christian Stahl and Karsten Wolf. Deciding Service Composition and Substitutability Using Extended Operating Guidelines. Data Knowl. Eng., 68(9): 819-833, 2009.

Abstract: We study the correct interaction between services using the following notion for correctness: there is no deadlock in the interaction of the services, and a given set of activities is not dead, that is, each activity in this set is executed in at least one run. The second condition has not been studied before. An operating guideline of a service P is an operational characterization of all deadlock-free interacting partners of P. In this paper, we present an extension of the concept of an operating guideline to characterize all correctly interacting partners of a service P. This extension can be used for answering at least the following two questions. First, given a service R, does R interact correctly with P? Second, given a service P', can P be substituted by P', that is, is every correctly interacting partner of P a correctly interacting partner of P', too?

Kees van Hee, Eric Verbeek, Christian Stahl, and Natalia Sidorova. A Framework for Linking and Pricing No-Cure-No-Pay Services. Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems, 2: 192-207, March 2009.

Abstract: In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.

Niels Lohmann, Peter Massuthe, Christian Stahl, and Daniela Weinberg. Analyzing Interacting WS-BPEL Processes Using Flexible Model Generation. Data Knowl. Eng., 64(1): 38-54, January 2008.

Abstract: We address the problem of analyzing the interaction between WS-BPEL processes. We present a technology chain that starts out with a WS-BPEL process and translates it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). To manage processes of realistic size, we present a concept of a \emph{flexible model generation} which allows the generation of compact Petri net models. A case study demonstrates the value of this technology chain.

Peter Massuthe, Alexander Serebrenik, Natalia Sidorova, and Karsten Wolf. Can I find a Partner? Undecidablity of Partner Existence for Open Nets. Information Processing Letters, 108(6): 374--378, November 2008.
Kathrin Kaschner, Peter Massuthe, and Karsten Wolf. Symbolic Representation of Operating Guidelines for Services. Petri Net Newsletter, 72: 21-28, April 2007.

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.

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.

Peter Massuthe and Karsten Wolf. Operating Guidelines for Services. Petri Net Newsletter, 70: 9-14, April 2006.

Abstract: In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester's service and the operating guideline.

Peter Massuthe, Wolfgang Reisig, and Karsten Schmidt. An Operating Guideline Approach to the SOA. Annals of Mathematics, Computing & Teleinformatics, 1(3): 35-43, 2005.

Abstract: Interorganizational cooperation is more andmore organized by the paradigm of services. The serviceoriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester's and provider's services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester's service and the operating guideline. Binding of a requester's and a provider's service is therefore guaranteed to result in a well-behaving cooperating service. At this time, the approach is limited to acyclic Petri nets.

Wolfgang Reisig, Karsten Schmidt, and Christian Stahl. Kommunizierende Workflow-Services modellieren und analysieren. Informatik - Forschung und Entwicklung, pp 90-101, October 2005.

Abstract: Zur ad�quaten Nutzung von Workflow-Implementierungen kommunizierender Gesch�ftsprozesse werden Konzepte vorgeschlagen,die von konkreten Implementierungen abstrahieren. Auf der Basis von Petrinetzen werden unterschiedliche Varianten der Bedienbarkeit von Workflows charakterisiert und daf�r Entscheidungsalgorithmen vorgestellt. Die Angemessenheit des Ansatzes wird am Beispiel der Semantik von Komponenten der Gesch�ftsprozess-Modellierungssprache BPEL demonstriert.

Bernd-Holger Schlingloff, Axel Martens, and Karsten Schmidt. Modeling and Model Checking Web Services. Electronic Notes in Theoretical Computer Science: Issue on Logic and Communication in Multi-Agent Systems, 126: 3-26, March 2005.

Abstract: We give an overview on web services and the web service technology stack. We then show how to build Petri net models of web services formulated in the specification language BPEL4WS. We define an abstract correctness criterion for these models and study the automated verification according to this criterion. Finally, we relate correctness of web service models to the model checking problem for alternating temporal logics.

Jose M. Vidal, Paul Buhler, and Christian Stahl. Multiagent Systems with Workflows. IEEE Internet Computing, 8(1): 76-82, February 2004.

Abstract: Industry and researchers have two different visions for the future of Web services. Industry wants to capitalize on Web service technology to automate business processes via centralized workflow enactment. Researchers are interested in the dynamic composition of Web services. The authors show how these two visions are points in a continuum and discuss a possible path for bridging the gap between them.

Axel Martens. On Compatibility of Web Services. Petri Net Newsletter, 65: 12-20, 2003.

Konferenzbeitr�ge und Beitr�ge auf Workshops

Dirk Fahland. A scenario is a behavioral view - Orchestrating services by scenario integration. In Oliver Kopp and Niels Lohmann, editors, Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, pages 8-14, March 2009. CEUR-WS.org.

Abstract: The construction of a complex service orchestration is a tedious and error-prone task as multiple service interactions with a single orchestrating service must be specified and combined. We suggest to specify a service orchestration in terms of behavioral scenarios that capture a specific aspect of service interaction, a behavioral view in isolation. By synchronizing the different scenarios, the views get integrated and define the behavior of a complex service orchestration. Our formal model for scenarios and their integration is a class of Petri nets called oclets.

Nannette Liske, Niels Lohmann, Christian Stahl, and Karsten Wolf. Another Approach to Service Instance Migration. In Luciano Baresi, Chi-Hung Chi, and Jun Suzuki, editors, Service-Oriented Computing - ICSOC 2009, 7th International Conference, Stockholm, Sweden, November 24-27, 2009. Proceedings, Lecture Notes in Computer Science, pages 607-621, November 2009. Springer-Verlag.

Abstract: Services change over time, be it for internal improvements, be it for external requirements such as new legal regulations. For long running services, it may even be necessary to change a service while instances are actually running and interacting with other services. This problem is referred to as instance migration. We present a novel approach to the behavioral (service protocol) aspects of instance migration. We apply techniques for finitely characterizing the set of all correctly interacting partners to a given service. The approach assures that migration does not introduce behavioral problems with any running partner of the original service. Our technique scales up to services with thousands of states, including models of real WS-BPEL processes.

Jarungjit Parnji, Christian Stahl, and Karsten Wolf. A finite representation of all substitutable services and its applications. In Oliver Kopp and Niels Lohmann, editors, Services and their Composition, 1st Central-European Workshop on, ZEUS 2009, Stuttgart, Germany, March 2--3, 2009, volume 438 of CEUR Workshop Proceedings, pages 8-14, March 2009. CEUR-WS.org.

Abstract: We present a finite representation of all substitutable services P' of a given service P. We show that our approach can be used for at least two applications: (1) given a finite set of services \mathcal{P} = {P1, ..., Pn}, we provide a representation of all services P' that can substitute every Pi \in \mathcal{P}, and (2) given a service P'' that cannot substitute a service P, we find the most similar service P* to P'' that can substitute P.

Jan S�rmeli. Profiling Services with Static Analysis. In AWPN, volume 501 of CEUR Workshop Proceedings, pages 35-40, 2009. CEUR-WS.org.

Karsten Wolf, Christian Stahl, Janine Ott, and Robert Danitz. Verifying Livelock Freedom in an SOA Scenario. In Stephen Edwards and Walter Vogler, editors, Proceedings of the Ninth International Conference on Application of Concurrency to System Design (ACSD'09), Augsburg, Germany, pages 168-177, July 2009. IEEE Computer Society.

Abstract: In a service-oriented architecture (SOA), a service broker assigns a previously published service (stored in a service registry) to a service requester. It is desirable for the composition of the requesting and the assigned service to interact properly. While proper interaction is often reduced to deadlock freedom of the composed system, we additionally consider livelock freedom as a desirable property for the interaction of services. In principle, deadlock- and livelock freedom can be verified by inspecting the state space of the composition of (public views of) the involved services. The contribution of this paper is to propose a methodology to build that state space from pre-computed fragments which are computed upon publishing a service. That way, we shift computation time from the time critical request phase of service brokerage to the less critical publish phase. Interestingly, our setting enables state space reduction methods that are intrinsically different from traditional state space reductions.

Wil M. P. van der Aalst, Arjan J. Mooij, Christian Stahl, and Karsten Wolf. Service Interaction: Patterns, Formalization, and Analysis. In Marco Bernardo, Luca Padovani, and Gianluigi Zavattaro, editors, Formal Methods for Web Services (SFM 2009), volume 5569, pages 42--88, April 2009. Springer-Verlag.

Abstract: As systems become more service oriented and processes increasingly cross organizational boundaries, interaction becomes more important. New technologies support the development of such systems. However, the paradigm shift towards service orientation, requires a fundamentally different way of looking at processes. This survey aims to provide some foundational notions related to service interaction. A set of service interaction patterns is given to illustrate the challenges in this domain. Moreover, key results are given for three of these challenges: (1) How to expose a service?, (2) How to replace and refine services?, and (3) How to generate service adapters? These challenges will be addressed in a Petri net setting. However, the results extend to other languages used in this domain.

Wil M. P. van der Aalst, Niels Lohmann, Peter Massuthe, Christian Stahl, and Karsten Wolf. From Public Views to Private Views -- Correctness-by-Design for Services. In Marlon Dumas and Reiko Heckel, editors, Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in Computer Science, pages 139-153, 2008. Springer-Verlag.

Abstract: Service orientation is a means for integrating across diverse systems. Each resource, whether an application, system, or trading partner, can be accessed as a service. The resulting architecture, often referred to as SOA, has been an important enabler for interorganizational processes. Apart from technological issues that need to be addressed, it is important that all parties involved in such processes agree on the "rules of engagement". Therefore, we propose to use a contract that specifies the composition of the public views of all participating parties. Each party may then implement its part of the contract such that the implementation (i.e., the private view) accords with the contract. In this paper, we define a suitable notion of accordance inspired by the asynchronous nature of services. Moreover, we present several transformation rules for incrementally building a private view such that accordance with the contract is guaranteed by construction. These rules include adding internal tasks as well as the reordering of messages and are therefore much more powerful than existing correctness-preserving construction rules.

Niels Lohmann. Correcting Deadlocking Service Choreographies Using a Simulation-Based Graph Edit Distance. In Marlon Dumas and Manfred Reichert, editors, Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1--4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, pages 132-147, September 2008. Springer-Verlag.

Abstract: Many work has been conducted to analyze service choreographies to assert manyfold correctness criteria. While errors can be detected automatically, the correction of defective services is usually done manually. This paper introduces a graph-based approach to calculate the minimal edit distance between a given defective service and synthesized correct services. This edit distance helps to automatically fix found errors while keeping the rest of the service untouched. A prototypic implementation shows that the approach is applicable to real-life services.

Wolfgang Reisig. Towards a Theory of Services. In Guenther Fliedl (Eds.) Roland Kaschek, Christian Kop, Claudia Steinberger, editor, Information Systems and e-Business Technologies, 2nd International United Information Systems Conference, UNISCON 2008, Klagenfurt, Austria, pages 22-25, April 2008. Springer-Verlag.

Abstract: Service-oriented Computing and Service-oriented Architectures aspire to better exploit existing middleware technologies. To this end, a more flexible, platform independent software design methodology is suggested, to develop rapid, low cost, interoperable, evolving and massively distributed software systems. Intended application areas include electronic commerce, information systems, supply chain control, and many other areas. Time is ripe to underpin this effort by theoretically well-founded concepts to model services, and to analyze such models. In this paper we suggest first proposals and principles for a comprehensive theory of services.

Chistian Stahl and Karsten Wolf. An Approach to Tackle Livelock-Freedom in SOA. In Niels Lohmann and Karsten Wolf, editors, Proceedings of the 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, Rostock, Germany, September 26--27, 2008, volume 380 of CEUR Workshop Proceedings, pages 69-74, September 2008. CEUR-WS.org.

Abstract: We calculate a fixed finite set of state space fragments for a service P, where each fragment carries a part of the whole behavior of P. By composing these fragments according to the behavior of a service R we build the state space of their composition P \oplus R which can be checked for deadlocks and livelocks. We show that this approach is applicable to realize a ``find'' request by a service $R$ with a provided service P in SOA.

Christian Stahl and Karsten Wolf. Covering Places and Transitions in Open Nets. In Marlon Dumas and Manfred Reichert, editors, Business Process Management, 6th International Conference, BPM 2008, Milan, Italy, September 1-4, 2008, Proceedings, volume 5240 of Lecture Notes in Computer Science, pages 116-131, September 2008. Springer-Verlag.

Abstract: We present a finite representation of all services M where the composition with a given service N is deadlock-free, and a given set of activities of N can be covered (i.e. is not dead). Our representation is an extension of the existing notion of an operating guideline which only cared about deadlock freedom. We further present an algorithm to decide whether a service M matches with the extended operating guideline of N.

Daniela Weinberg. Efficient Controllability Analysis of Open Nets. In Roberto Bruni and Karsten Wolf, editors, Web Services and Formal Methods, Fifth International Workshop, WS-FM 2008, Milan, Italy, September 4--5, 2008, Proceedings, Lecture Notes in Computer Science, September 2008. Springer-Verlag.

Abstract: A service is designed to interact with other services. If the service interaction is stateful and asynchronous, the interaction protocol can become quite complex. A service may be able to interact with a lot of possible partner services, one partner or no partner at all. Having no partner surely is not intended by the designer. But the stateful interaction between services can be formalized and thus analyzed at design time. We present a formalization which is centered around a graph data structure that we call interaction graph, which represents feasible runs of a partner service according to the interaction protocol. As interaction graphs suffer from state explosion, we introduce a set of suitable reduction rules to alleviate the complexity of our approach. As our case studies show we are able to analyze the interaction behavior of a service efficiently.

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.

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.

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.

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.

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.

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.

Kathrin Kaschner, Peter Massuthe, and Karsten Wolf. Symbolische Repr�sentation von Bedienungsanleitungen f�r Services. In Daniel Moldt, editor, 13. Workshop Algorithmen und Werkzeuge f�r Petrinetze (AWPN 2006), Proceedings, pages 54-61, September 2006. Universit�t Hamburg. Note: In German.
Oliver Kopp, Carsten Frenkler, and Niels Lohmann. Korrektheit und Zuverl�ssigkeit zusammengesetzter Web Services am Beispiel der Gesch�ftsprozess-Modellierungssprache BPEL. In Forschungsoffensive ''Software Engineering 2006'', Statuskonferenz, 26.-28. Juni 2006, July 2006. Bundesministerium f�r Bildung und Forschung (BMBF).

Niels Lohmann, Peter Massuthe, Christian Stahl, and Daniela Weinberg. Analyzing Interacting BPEL Processes. In Schahram Dustdar, Jos� Luiz Fiadeiro, and Amit Sheth, editors, Business Process Management, 4th International Conference, BPM 2006, Vienna, Austria, September 5-7, 2006, Proceedings, volume 4102 of Lecture Notes in Computer Science, pages 17-32, September 2006. Springer-Verlag.

Abstract: This paper addresses the problem of analyzing theinteraction between BPEL processes. We present a technology chain that starts out with a BPEL process and transforms it into a Petri net model. On the model we decide controllability of the process (the existence of a partner process, such that both can interact properly) and compute its operating guideline (a characterization of all properly interacting partner processes). A case study demonstrates the value of this technology chain.

Peter Massuthe and Karsten Wolf. An Algorithm for Matching Nondeterministic Services with Operating Guidelines. In Frank Leymann, Wolfgang Reisig, Satish R. Thatte, and Wil M. P. van der Aalst, editors, The Role of Business Processes in Service Oriented Architectures, number 06291 of Dagstuhl Seminar Proceedings, 2006. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany.

Abstract: Interorganizational cooperation is more and more organized 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 nondeterministic 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 artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlock-free communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.

Wolfgang Reisig, Dirk Fahland, Niels Lohmann, Peter Massuthe, Christian Stahl, Daniela Weinberg, Karsten Wolf, and Kathrin Kaschner. Analysis Techniques for Service Models. In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006 (ISoLA 2006), 15-19 November 2006, Paphos, Cyprus, pages 11-17, November 2006. IEEE Computer Society.

Abstract: The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. To make sure that our models properly reflect real world issues of services, we model and investigate services represented in established languages such as WS-BPEL.

Dirk Fahland and Wolfgang Reisig. ASM-based semantics for BPEL: The negative Control Flow. In Dani�le Beauquier, Egon B�rger, and Anatol Slissenko, editors, Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), pages 131-151, March 2005. Paris XII.

Abstract: BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.

Sebastian Hinz, Karsten Schmidt, and Christian Stahl. Transforming BPEL to Petri Nets. In Wil M. P. van der Aalst, B. Benatallah, F. Casati, and F. Curbera, editors, Proceedings of the Third International Conference on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, Nancy, France, pages 220-235, September 2005. Springer-Verlag.

Abstract: We present a Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics covers the standard behaviour of BPEL as well as the exceptional behaviour (e.g. faults, events, compensation). The semantics is implemented as a parser that translates BPEL specifications into the input language of the Petri net model checking tool LoLA. We demonstrate that the semantics is well suited for computer aided verification purposes.

Axel Martens. Analyzing Web Service based Business Processes. In Maura Cerioli, editor, Proceedings of Intl. Conference on Fundamental Approaches to Software Engineering (FASE'05), Part of the 2005 European Joint Conferences on Theory and Practice of Software (ETAPS'05), volume 3442 of Lecture Notes in Computer Science, Edinburgh, Scotland, April 2005. Springer-Verlag.

Abstract: This paper is concerned with the application of Web services to distributed, cross-organizational business processes. In this scenario, it is crucial to answer the following questions: Do two Web services fit together in a way such that the composed system is deadlock-free? - the question of compatibility. Can one Web service be replaced by another while the remaining components stay untouched? - the question of equivalence. Can we reason about the soundness of one given Web service without considering the actual environment it will by used in? This paper defines the notion of usability - an intuitive and locally provable soundness criterion for a given Web services. Based on this notion, this paper demonstrates how the other questions could be answered. The presented method is based on Petri nets, because this formalism is widely used for modeling and analyzing business processes. Due to the existing Petri net semantics for BPEL4WS - a language that is in the very act of becoming the industrial standard for Web service based business processes - the results are directly applicable to real world examples.

Axel Martens. Process Oriented Discovery of Business Partners. In Proceedings of 7th Intl. Conference on Enterprise Information Systems (ICEIS'05), Vol 3, Miami, Florida, May 2005. INSTICC.

Abstract: Emerging technologies and industrial standards in the field of Web services enable a much faster and easier cooperation of distributed partners. With the increasing number of enterprises that offer specific functionality in terms of Web services, discovery of matching partners becomes a serious issue. At the moment, discovery of Web services generally is based on meta-information (e. g. name, business category) and some technical aspects (e. g. interface, protocols). But, this selection might be to coarse grained for dynamic application integration, and there is much more information available. This paper describes a method to discover business partners based on the comparison of their behavior ? specified in terms of their published Web service process models.

Peter Massuthe and Karsten Schmidt. Operating Guidelines - an Automata-Theoretic Foundation for the Service-Oriented Architecture. In Kai-Yuan Cai, Atsushi Ohnishi, and M.F. Lau, editors, Proceedings of the Fifth International Conference on Quality Software (QSIC 2005), Melbourne, Australia, pages 452-457, September 2005. IEEE Computer Society.

Abstract: In the service-oriented architecture (SOA), we distinguish three roles of service owners: service providers, service requesters, and service brokers. Each service provider publishes information to the broker about how requesters can interact with its service. Thus, the broker can assign a fitting service provider to a querying requester. We propose the information published to the broker to be operating guidelines. Operating guidelines are essentially communication instructions for the service requester. We present an automata-theoretic approach that is centered around operating guidelines and is capable of implementing all tasks arising in the SOA.

Peter Massuthe and Karsten Schmidt. Operating Guidelines for Services. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop Algorithmen und Werkzeuge f�r Petrinetze (AWPN 2005), Proceedings, pages 78-83, September 2005. Humboldt-Universit�t zu Berlin.

Abstract: In the service-oriented architecture (SOA), we distinguish three roles of service owners:service providers, service requesters, and service brokers, and the three standard operations publish, find, and bind. We provide a formal method based on Petri nets to model services. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline.

Wolfgang Reisig. Modeling- and Analysis Techniques for Web Services and Business Processes. In Martin Steffen and Gianluigi Zavattaro, editors, Formal Methods for Open Object-Based Distributed Systems: 7th IFIP WG 6.1 International Conference, FMOODS 2005, Athens, Greece, June 15-17, 2005. Proceedings, volume 3535 of Lecture Notes in Computer Science, pages 243-258, May 2005. Springer Verlag.

Abstract: Open distributed systems include in particular Web services and business processes. There is a need of techniques to model such systems formally, and to derive decisive properties from such models. Three such techniques are presented in this paper, exemplified by help of realistic examples, and mutually related w.r.t. their respective expressive power and the availability of analysis techniques.

Daniela Weinberg and Karsten Schmidt. Reduction Rules for Interaction Graphs. In Karsten Schmidt and Christian Stahl, editors, 12. Workshop Algorithmen und Werkzeuge f�r Petrinetze (AWPN 2005), Proceedings, pages 60-65, September 2005. Humboldt-Universit�t zu Berlin.

Abstract: The internet today has grown to be more than just being a basisfor exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules are implemented and have been integrated into an analysis tool kit for web services.

Axel Martens. Analysis and re-engineering of Web Services. In Proceedings of 6th International Conference on Enterprise Information Systems (ICEIS'04), 2004. Porto, Portugal.

Abstract: To an increasing extend software systems are integrated across the borders of individual enterprises. The Web Service approach provides group of technologies to describe components and their composition, based on well established protocols. Focused on business processes, one Web Service implements a local subprocess. A distributed business processes is implemented by the composition a set of communicating Web Services. At the moment, there are various modeling languages under development to describe the internal structure of one Web Service (e. g. Business Process Execution Language for Web Services BPEL4WS (BEA et al., 2002a)) and the choreography of a set of Web Services (e. g. Web Service Choreography Interface WSCI (BEA et al., 2002b)). Nevertheless, there is a need for methods for stepwise construction and verification of such components. This paper abstracts from concrete syntax of any proposed language definition. Instead, we apply Petri nets to model Web Services. Thus, we are able to reason about essential properties, e. g. usability of a Web Service - our notion of a quality criterion. Based on this framework, we present an algorithm to analyze a given Web Service and to transfer a complex process model into a appropriate model of a Web Service.

Karsten Schmidt. Distributed Usability of Web Services. In Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN 04), pages 19-24, 2004. Bericht tr-ri-04-251, Universit�t Paderborn.

Abstract: We estabilish a theory of distributed usability. To do so, it is however neccessary to modify the already existing theory of central usability.

Axel Martens. Compatibility of Web Services. In 10th Workshop on Algorithms and Tools for Petri Nets (AWPN 2003), Eichst�tt, Germany, pages 26.-27, September 2003.

Abstract: To an increasing extend business processes run across the borders of individual enterprises. Thus, there is a need to map each local subprocess into a self-contained component; a distributed business process arises from composition of such component via standardized communication protocols. The Web service approach provides a standardized, platform independent and widely accepted concept of components and composition for distributed systems of all kinds. This approach comes along together with group of technologies to describe precisely the structure of one Web service and the composition of a set of Web services. Although the technological basement is given, there is a lot of open questions, e. g. semantic compatibility of two Web services. This paper abstracts from concrete syntax of any proposed language definition. Instead, we apply Petri nets to model Web services. Thus, we are able to reason about essential properties, e. g. usability of a Web service - our notion of a quality criterion. Based on this framework, we discuss and define a criterion for semantic compatibility of Web services.

Axel Martens. On Usability of Web Services. In Coral Calero, Oscar D�az, and Mario Piattini, editors, Proceedings of 1st Web Services Quality Workshop (WQW 2003), Rome, Italy, 2003.

Abstract: This paper is concerned with the application of Web services to distributed, cross-organizational business processes. Web services provide a platform independent concept of components and composition. Thus, they seem to be a proper technology to cover the heterogenous structures within distributed business processes: One Web service realizes a local subprocess. A distributed business process is realized by the composition of a set of Web services. Although the technological basement is given, there is a lot of open questions: Do two Web services fit together in a way, that the composition yields a deadlock-free system? - the question of compatibility. Can one Web service be exchanged by another within a composed system without running into problems? - the question of equivalence. Can we reason about the quality of one given Web service without considering the environment it will by used in? In this paper we present the notion of usability - our quality criterion of a Web service. This criterion is intuitive and can be easily proven locally. Moreover, this notion allows to answer the other questions mentioned above. The approach and the results presented in this paper are taken from a larger framework for modeling and analyzing business processes by help of Web services published in my PhD thesis [9].

Technische Berichte

Christian Gierds, Arjan J. Mooij, and Karsten Wolf. Specifying and generating behavioral service adapter based on transformation rules. Preprint CS-02-08, Universit�t Rostock, Rostock, Germany, August 2008.

Abstract: Behavioral adapters are a way to establish proper interaction between services that have been developed independently. We present a novel approach for specifying such adapters, based on domain-specific transformation rules that reflect the elementary operations that adapters can perform. We show how complex adapters that adhere to these rules can be generated using existing controller generation algorithms. We discuss some example applications, including real-world business processes.

Peter Massuthe, Alexander Serebrenik, Natalia Sidorova, and Karsten Wolf. Can I find a Partner?. Preprint CS-01-08, Universit�t Rostock, Rostock, Germany, March 2008.

Abstract: We study open nets as Petri net models of web services, with a link to the practically relevant language WS-BPEL. For those nets, we investigate the problem of serviceableness which we consider as fundamental as the successful notion of soundness for workflow nets, i.e. Petri net models of business processes and workflows. While we could give algorithmic solutions to the serviceableness problem for subclasses of open nets in earlier work, this article shows that the problem is in general undecidable.

Christian Stahl, Peter Massuthe, and Jan Bretschneider. Deciding Substitutability of Services with Operating Guidelines. Informatik-Berichte 222, Humboldt-Universit�t zu Berlin, April 2008.

Abstract: Deciding whether a service $S$ can be substituted by another service S' is an important problem in practice and one of the research challenges in service-oriented computing. In this paper, we define three substitutability notions for services. Accordance specifies that S' cooperates with at least the environments that S cooperates with. S and S' are equivalent if they cooperate with the same environments. To guarantee that S' cooperates with a fixed subset of environments that S cooperates with, the notion of deprecation can be used. For each substitutability notion we present a decision algorithm. To this end we apply the concept of an operating guideline of a service as an abstract representation of all environments the service cooperates with.

Kees M. van Hee, H.M.W. Verbeek, Christian Stahl, and Natalia Sidorova. A Framework for Linking and Pricing No-Cure-No-Pay Services. Computer Science Report 08/19, Technische Universiteit Eindhoven, Eindhoven, The Netherlands, June 2008.

Abstract: In this paper, we present a framework that allows us to orchestrate web services such that the web services involved in this orchestration interact properly. To achieve this, we predefine service interfaces and certain routing constructs. Furthermore, we define a number of rules to incrementally compute the price of such a properly interacting orchestration (i.e. a web service) from the price of its web services. The fact that a web service gets only payed after its service is delivered (no-cure-no-pay) is reflected by considering a probability of success. To determine a safe price that includes the risk a web service takes, we consider the variance of costs.

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.

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.

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.

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.

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.

Niels Lohmann, Peter Massuthe, and Karsten Wolf. Operating Guidelines for Finite-State Services. Informatik-Berichte 210, Humboldt-Universit�t zu Berlin, December 2006.

Abstract: We introduce the concept of an operating guideline for an arbitrary finite-state service P, extending the work of [1, 2] which was restricted to acyclic services. An operating guideline gives complete information about how to correctly (in this paper: deadlock-free) communicate with P. It can further be executed or used for service discovery. An operating guideline for P is a particular service S that is enriched with annotations. S communicates deadlock-free with P and is able to simulate every other service that communicates deadlock-free with P. The attached annotations give complete information about whether or not a simulated service is deadlock-free, too.

Peter Massuthe and Karsten Wolf. An Algorithm for Matching Nondeterministic Services with Operating Guidelines. Informatik-Berichte 202, Humboldt-Universit�t zu Berlin, 2006.

Abstract: Interorganizational cooperation is more and more organizedby 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 nondeterministic 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 artifact to realize the publish operation. In our approach, the find operation reduces to a matching problem between the requester's service and the published operating guidelines. If matching services are actually bound together, our approach guarantees deadlockfree communication. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.

Daniela Weinberg. Reduction Rules for Interaction Graphs. Informatik-Berichte 198, Humboldt-Universit�t zu Berlin, February 2006.

Abstract: The internet today has grown to be more than just being a basis for exchanging information. It steadily becomes a platform for processing business processes. Many companies distribute their service with the help of web services or integrate other web services into their own workflow. However, before a web service gets published it should be examined well. We will introduce a way of examining the controllability of a web service. That means, we study whether a controller can actually use the functionality provided by the web service. We propose the interaction graph of a web service, that is modelled by an open workflow net. To verify whether such a net is controllable or not it is sufficient to construct a reduced interaction graph. We will define reduction rules that minimize the size of the graph greatly. The analysis using the interaction graph as well as the reduction rules shown in this paper are implemented and have been integrated into an analysis tool kit for web services.

Dirk Fahland. Complete Abstract Operational Semantics for the Web Service Business Process Execution Language. Informatik-Berichte 190, Humboldt-Universit�t zu Berlin, September 2005.

Abstract: In this technical report we present an abstract operational semantics for the Business ProcessExecution Language for Web Services, or BPEL for short. In effect, the semantics defined herein are a variation and an extension of the semantics published first in [FGV04a] and [Far04] defined by the group of Uwe Gl�sser the Simon Fraser University, Vancouver, Canada. We namely add semantics for correlation handling, dead path elimination and event handling; we define the data handling on a finer level; we slightly alter the basic framework of how activities are formalized in [FGV04a] in order to achieve greater robustness against changes of the informal specification. Furthermore this technical report serves as a base for a joint work with the group of Simon Fraser University.

Peter Massuthe, Wolfgang Reisig, and Karsten Schmidt. An Operating Guideline Approach to the SOA. Informatik-Berichte 191, Humboldt-Universit�t zu Berlin, 2005.

Abstract: Interorganizational cooperation is more and more organized by the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the three operations publish, find, and bind. We provide a formal method based on Petri nets to model services and their cooperation. We characterize well-behaving pairs of requester?s and provider?s services and suggest operating guidelines as a convenient and intuitive artifact to realize publish. Then, the find operation reduces to a matching problem between the requester?s service and the operating guideline. Binding of a requester?s and a provider?s service is therefore guaranteed to result in a well-behaving cooperating service.

Peter Massuthe and Karsten Schmidt. Matching Nondeterministic Services with Operating Guidelines. Informatik-Berichte 193, Humboldt-Universit�t zu Berlin, June 2005.

Abstract: Abstract Interorganizational cooperation is more and more organizedby the paradigm of services. The service-oriented architecture (SOA) provides a general framework for service interaction. It describes three roles, service provider, service requester, and service broker, together with the operations publish, find, and bind. We provide a formal method based on nondeterministic automata to model services and their interaction. We suggest operating guidelines as a convenient and intuitive artifact to realize publish. In our approach, the find operation reduces to a matching problem between the requester?s service and operating guidelines. In this paper, matching of deterministic as well as nondeterministic automata with operating guidelines is presented.

Peter Massuthe and Karsten Schmidt. Operating Guidelines - an Alternative to Public View. Informatik-Berichte 189, Humboldt-Universit�t zu Berlin, 2005.

Abstract: We propose operating guidelines as artifacts for publishing information about how to communicate with a business process that is intended to be provided as a service. We present an approach to compute operating guidelines fully automatically. We compare operating guidelines with the concept of public view.

Wolfgang Reisig. Modeling- and Analysis Techniques for Web Services and Business Processes. Informatik-Berichte 183, Humboldt-Universit�t zu Berlin, 2005.

Christian Stahl. A Petri Net Semantics for BPEL. Informatik-Berichte 188, Humboldt-Universit�t zu Berlin, July 2005.

Abstract: We present a pattern-based Petri net semantics for the Business Process Execution Language for Web Services (BPEL). Our semantics is complete - it covers the standard behaviour of BPEL as well as the exceptional behav-iour (e.g. faults, events, compensation). Therefore every business process specified in BPEL can be transformed into a Petri net.

Axel Martens, Christian Stahl, Daniela Weinberg, Dirk Fahland, and Thomas Heidinger. Business Process Execution Language for Web services - Semantik, Analyse und Visualisierung. Informatik-Berichte 169, Humboldt-Universit�t zu Berlin, July 2004.

Abstract: Moderne Systeme der Informationstechnik bestehen zumeist aus einer Vielzahl von Komponenten, die in einem Netzwerk auf verteilten Knoten ausgef�hrt werden. Mit dem Web-Service-Ansatz k�nnen solche Systeme einfacher und flexibler entwickelt werden. Diese Arbeit befasst sich mit der Modellierung, Visualisierung und Analyse von Web Services. Ein Web Service kapselt eine Anwendung und stellt diese �ber ein wohldefiniertes Interface der Au�enwelt zur Verf�gung. Im Gegensatz zu fr�heren Ans�tzen dienen eine Reihe zusammenh�ngender Technologien zur Beschreibung eines Web Service. Diese Arbeit besch�ftigt sich vor allem mit der internen Struktur eines Web Service, beschrieben mit Hilfe der Business Process Execution Language for Web Services (BPEL4WS) [ACD+02]. Der Web-Service-Ansatz bietet ein homogenes Konzept von Komponenten und ihrer Komposition ber einem heterogenen Netzwerk. Damit ist die syntaktische Grundlage f�r die Entwicklung verteilter Systeme gelegt. Wesentlich f�r den Erfolg der Web Services ist jedoch die Beantwortung der semantischen Fragestellungen: Passen zwei gegebene Web Services inhaltlich zusammen? Kann in einem verteilten System ein gegebener Web Service durch einen anderen ersetzt werden? Entspricht ein konkreter Web Service einer gegebenen abstrakten Spezifikation? Diese Arbeit befasst sich mit der Beantwortung dieser und weiterer Fragestellungen im Web-Service-Ansatz: In einem ersten Schritt entwickeln wir eine formale Semantik f�r die Sprache BPEL4WS. Darauf aufbauend werden Methoden zur Analyse verteilter Systeme auf die konkreten Anforderungen bertragen und neue Verfahren entwickelt. F�r die Diskussion der Modelle und Eigenschaften entwickeln wir eine intuitive graphische Repr�sentation der Sprache BPEL4WS. Das Ziel der Forschungen ist die Umsetzung der Methoden in einem integrierten Entwicklungswerkzeug f�r BPEL4WS. Die vorliegende Arbeit beschreibt die ersten Ergebnisse in einem laufenden Projekt.

Wolfgang Reisig and A. Brade. ASM Models for Web Services. Informatik-Berichte 181, Humboldt-Universit�t zu Berlin, 2004.

Studien- und Diplomarbeiten

Katharina G�rlach. Ein Verfahren zur abstrakten Interpretation von XPath-Ausdr�cken in WS-BPEL-Prozessen. Diplomarbeit, Humboldt-Universit�t zu Berlin, March 2008.

Abstract: Die Web Services Business Process Execution Language ist eine Sprache zur Modellierung von Gesch�ftsprozessen als Web Services. F�r eine umfassende Analyse von WS-BPEL-Prozessen m�ssen auch die Daten der Prozesse analysiert werden. Daten werden in WS-BPEL-Prozessen mit Hilfe von XML-Schema typisiert und standardm��ig mit Hilfe von XPath manipuliert. Eine Datenanalyse f�r WS-BPEL muss deshalb XML-Schema ber�cksichtigen die im Prozess enthaltenen XPath-Ausdr�cke auswerten. Eine solche Datenanalyse erm�glicht R�ckschl�sse auf den Kontrollfluss und dient so beispielsweise zur Optimierung eines WS-BPEL-Prozesses. In der vorliegenden Arbeit wird ein Verfahren zur abstrakten Interpetation von XPath-Ausdr�cken in WS-BPEL-Prozessen vorgestellt. Daf�r wird ein umfassendes Datenmodell f�r WS-BPEL-Prozesse sowie die enthaltenen XPath-Ausdr�cke entwickelt. Auf Grundlage des entwickelten Datenmodells stellen wir eine statische Analyse vor, die die XPath-Ausdr�cke in einem WS-BPEL-Prozess abstrakt interpretiert. Die Analyse berechnet dabei die Wertebereiche f�r Variablen und Bedingungen in WS-BPEL-Prozessen.

Patrick K�hnen. Synthese offener Workflownetze aus Serviceautomaten. Diplomarbeit, Humboldt-Universit�t zu Berlin, January 2008.

Abstract: Das Paradigma der service-orientierten Architektur beschreibt eine Kapselung einzelner Funktionalit�ten von Softwaresystemen in Services. Ein Service besitzt somit eine bestimmte Funktionalit�t und zudem eine definierte Schnittstelle. �ber diese Schnittstelle kann die Funktionalit�t des Services genutzt werden. Durch diese Trennung von Funktionalit�t und Schnittstelle ist ein Service unabh�ngig von der Plattform und der verwendeten Programmiersprache. �nderungen und Erweiterungen service-basierter Softwaresysteme k�nnen durch Anpassungen oder das Austauschen des betreffenden Services erreicht werden und sind daher im Vergleich zu anderen Systemen einfacher, schneller und mit einem geringeren Risiko umsetzbar. Web Services sind eine spezielle und weit verbreitete Form von Services. Ein Web Service ist ein eigenst�ndiges Softwaremodul, dessen Funktionalit�t �ber das Internet angeboten wird. Mit der Web Service Business Process Execution Language (WS-BPEL) kann ein Web Service definiert werden, der den Gesch�ftsprozess eines Unternehmens abbildet. WS-BPEL besitzt hierf�r Konstrollstrukturen und Funktionalit�t zur Behandlung von Fehlern und Ausnahmen. WS-BPEL besitzt keine formale Semantik und kann daher nicht formal analysiert werden. F�r eine formale Analyse kann ein WS-BPEL Prozess in ein offenes Workflownetz (oWFN) �bersetzt werden. Existiert f�r ein oWFN ein Partner, der verklemmungsfrei mit diesem oWFN interagiert, kann ein Serviceautomat (SVA) berechnet werden, der das Verhalten dieses Partners beschreibt. Bisher war es m�glich, ein oWFN nach WS-BPEL zu �bersetzen, aber nicht, ein oWFN aus einem SVA zu synthetisieren. Ein berechneter Partner f�r einen WS-BPEL Prozess in Form eines SVAs konnte somit bisher nicht zur�ck in WS-BPEL �bersetzt werden. Das Ziel dieser Arbeit ist es, die Synthese eines oWFNS aus einem SVA zu definieren und somit den Vorgang der Berechnung eines Partners f�r einen WS-BPEL Prozesss zu vervollst�ndigen.

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.

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.

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.

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.

Nannette Liske. Laufzeitersetzbarkeit von Services. Studienarbeit, Humboldt-Universit�t zu Berlin, April 2007.
Alexander Schulz. Zielgerichtete Strategien. Studienarbeit, Humboldt-Universit�t zu Berlin, July 2007.

Kathrin Kaschner. BDD-basiertes Matching von Services. Diplomarbeit, Humboldt-Universit�t zu Berlin, Mathematisch-Naturwissenschaftliche Fakult�t II, March 2006.

Abstract: Moderne Software-Systeme werden zunehmend nach dem Paradigma der ServiceorientiertenArchitektur (SOA) aus unabh�ngigen Services zusammengesetzt, die definierte Funktionen zur Verf�gung stellen und Nachrichten miteinander austauschen. Eine M�glichkeit zur Gew�hrleistung der reibungslosen Kommunikation besteht in der Bereitstellung einer Bedienungsanleitung durch den Service Provider, mit der der Service Broker anhand eines Pr�fverfahrens - dem Matching - entscheiden kann, ob der Service eines Service Requesters zu dem angebotenen Service passt. F�r die praktische Anwendung m�ssen Bedienungsanleitungen in geeigneter Weise kodiert werden. In der vorliegenden Arbeit werden dazu Bin�re Entscheidungsdiagramme (BDDs) genutzt. F�r das Matching wird der Service des Service Requesters durch einen Serviceautomaten modelliert, der seinerseits ebenfalls in eine BDD-Darstellung �berf�hrt wird. Darauf aufbauend wird schlie�lich ein Matching-Algorithmus entwickelt und seine Korrektheit bewiesen. Die Effizienz der Kodierung durch BDDs und die Funktionsweise des BDD-basierten Matching-Algorithmus wird an Beispielen gezeigt.

Jens Kleine. Abstrakte Petrinetzmuster f�r BPEL unter Bewahrung von Verklemmungen. Studienarbeit, Humboldt-Universit�t zu Berlin, October 2006.

Abstract: Wir pr�sentieren die Reduktion einer Petrinetzsemantik f�r die Business Process Execution Language for Web Services, die alle Verklemmungen bewahrt und dabei die Petrinetzmuster so stark verkleinert, dass Model-Checking gr��erer Gesch�ftsprozesse erm�glicht wird. Dies geschieht, indem wir jedes Petrinetzmuster einzeln betrachten und verkleinern. Bisherige Versuche der computergest�tzten Analyse scheiterten auf Grund der Gr��e und Komplexit�t der entstandenen Petrinetze.

Peter Laufer. Grundlagen f�r die Anpassung der Petrinetz-Semantik an WS-BPEL 2.0. Studienarbeit, Humboldt-Universit�t zu Berlin, May 2006.

Abstract: Die Business Process Execution Language for Web Services (BPEL) ist eine Sprache zur Definitionvon Gesch�ftsprozessen als Web Services. Um Eigenschaften eines BPEL-Prozesses verifizieren zu k�nnen, entwickelte Stahl eine Transformation von BPEL4WS 1.1 in Petrinetze. Als Ergebnis des Standardisierungsprozesses von BPEL wird demn�chst die Version WS-BPEL 2.0 verabschiedet werden. Da auch WS-BPEL 2.0 eine textuelle informelle Spezifikation zugrunde liegen wird, w�re eine angepasste Petrinetz-Semantik f�r Verifikationszwecke weiterhin sehr hilfreich. Ziel dieser Arbeit ist es deshalb, die nderungen von WS-BPEL 2.0 im Vergleich zum Vorg�nger BPEL4WS 1.1 zu dokumentieren und Vorschl�ge in Bezug auf die Anpassung der vorhandenen Petrinetz-Semantik zu geben. Die Betrachtungen beziehen sich dabei auf eine Entwurfsfassung der kommenden Spezifikation von WS-BPEL 2.0 vom 16. M�rz 2006.

Alexander Brade. ASMs und die Struktur und Dynamik von Web Services. Studienarbeit, Humboldt-Universit�t zu Berlin, January 2005.

Alexander Brade. �bersetzung graphischer Verhaltensbeschreibungen von Services in Abstract State Machines. Diplomarbeit, Humboldt-Universit�t zu Berlin, September 2005.

Abstract: Zu Beginn dieser Arbeit werden wir kurz die Begriffe Service OrientedArchitecture und Service erkl�ren. Den Begriff der Services werden wir genauer betrachten. Im Anschluss daran werden wir die Frage behandeln, wie das dynamische Verhalten eines Services mit UML 2-Diagrammen (UML = Unified Modeling Language) graphisch beschrieben werden kann. Dazu werden wir uns besonders auf die UML 2-Verhaltensdiagramme konzentrieren. Dabei werden wir auch einige Einschr�nkungen an den Verhaltensdiagrammen vornehmen. Wir werden dann das dynamische Verhalten eines beispielhaften DinnerServices mit Hilfe von Verhaltensdiagrammen beschreiben. Diese Verhaltensdiagramme des DinnerServices werden wir in Abstract State Machines (ASMs) �bersetzen. Zwei der so erhaltenen ASMs werden wir im Anschluss an die Verhaltensbeschreibungen des DinnerServices in die Spezifikationssprache AsmL �berf�hren und simulieren. Abschlie�end betrachten wir kurz die Verfeinerungsm�glichkeiten von ASMs.

Dirk Fahland. Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines. Studienarbeit, Humboldt-Universit�t zu Berlin, August 2004.

Abstract: In dieser Arbeit stellen wir einen Ansatz zur Definition einer formalen Semantik f�r die Business Process Execution Language for Web Services (kurz BPEL4WS) von IBM, Microsoft und deren Industriepartnern vor. Zur Formalisierung w�hlen wir den Abstract-State-Machine-Formalismus (kurz ASM), dessen theoretische Fundierung es uns erlaubt, die Semantik von BPEL4WS auf der selben Abstraktionsebene zur formalisieren, die in der informalen BPEL4WS-Spezifikation vorgegeben ist. Wir werden den inneren Aufbau der Sprache pr�zise, formal abbilden und damit eine intuitiv und anschaulich nachvollziehbare Entsprechung zwischen den Abl�ufen eines BPEL4WSProzesses gem�� der gegebenen informalen Semantik und unserer formalen Semantik aufzeigen. Dazu analysieren wir die Struktur von BPEL4WS und zeigen mit welchen Mitteln des ASM-Formalismus diese ad�quat, formal erfasst werden und wie in ASM notierte Spezifikationen zu lesen sind. Hierzu werden wir beispielhaft ausgew�hlte, syntaktische Konstrukte von BPEL4WS nach unserem Ansatz formalisieren. Die vorliegende Arbeit bezieht sich auf die informale BPEL4WS-Spezifikation v1.1, ver�ffentlicht am 5. Mai 2003.

Christian Stahl. Transformation von BPEL4WS in Petrinetze. Diplomarbeit, Humboldt-Universit�t zu Berlin, April 2004.

Abstract: BPEL4WS ist eine Sprache zur Beschreibung verteilter Gesch�ftsprozesse mit Web Services. Es besteht die Notwendigkeit, die Sprache trotz ihrer Komplexit�t zu verstehen, um mit ihr im Umfeld von Web Services arbeiten zu k�nnen. Mit Hilfe einer formalen Semantik ist es m�glich, die Sprache selbst und mit BPEL4WS spezifizierte Gesch�ftsprozesse zu verifizieren. In der vorliegenden Arbeit wird eine Petrinetz-Semantik f�r BPEL4WS vorgestellt. Dazu wird gezeigt, dass jedes Konstrukt der Sprache BPEL4WS in ein Petrinetz-Muster �bersetzt werden kann. Damit ist es m�glich, jeden in der Gesch�ftsprozesssprache BPEL4WS modellierten Gesch�ftsprozess in ein Petrinetz zu transformieren. Bei der Entwicklung der Semantik kann auf Forschungsergebnisse aus dem Bereich "Petrinetze als Werkzeug zur Gesch�ftsprozessmodellierung" zur�ckgegriffen werden.

Daniela Weinberg. Analyse der Bedienbarkeit. Diplomarbeit, Humboldt-Universit�t zu Berlin, October 2004.

Abstract: Das heutige Internet w�chst zunehmend von einer Plattform als Informationsquelle hin zu einer Basis f�r die Abwicklung von Gesch�ftsprozessen. Zahlreiche Firmen stellen ihre Dienste bereits mit Hilfe von Web-Services zur Verf�gung oder integrieren andere bereitgestellte Web-Services in ihren Gesch�ftsablauf. Nach Studien einiger Forschungsinstitute geht der Trend in der heutigen IT-Branche stark zum Einsatz solcher verteilter Gesch�ftsprozesse. Es werden Schlagworte wie out-tasking, plug-and-play und Lego-Wirtschaft gepr�gt. Bevor ein Gesch�ftsprozess in Form eines Web-Services jedoch ver�ffentlicht wird, sollte dieser geeignet untersucht werden. Wir werden uns in dieser Arbeit diesem Thema mit Hilfe von Petri-Netz-Modulen n�hern. Sie modellieren gerade die interne Struktur von Gesch�ftsprozessen und erm�glichen es, den Prozess geeignet zu analysieren. Uns interessiert bei der Analyse, ob die Funktionalit�t, die ein Web-Service bereitstellen soll, auch wirklich genutzt werden kann. Wir sprechen in diesem Zusammenhang von Bedienbarkeit. F�r die Analyse definieren wir den Interaktionsgraphen eines Workflow-Moduls, welcher die Zust�nde des Moduls und dessen Interaktion mit einer Umgebung veranschaulicht. Auf dieser Grundlage k�nnen wir dann eine Bedienstrategie definieren, durch die das Modul bedient werden kann. Das hei�t, wenn eine Umgebung das Modul so bedienen kann, dass dieses ordentlich terminiert, finden wir eine Bedienstrategie in dem Interaktionsgraphen des Moduls. Dar�ber hinaus bieten die Graphen dem Modellierer die M�glichkeit, einen Blick auf die Abl�ufe seines Moduls zu werfen und genau erkennen zu k�nnen, welche Zust�nde des Moduls bei welcher Interaktion mit der Umgebung eingenommen werden. Auf Grundlage dieser Analyse kann der Modellierer seinen Prozess �berarbeiten, anpassen etc. Um die Bedienbarkeit der Workflow-Module durch den Interaktionsgraphen zu verifizieren, reicht es aus, einen reduzierten Graphen zu konstruieren. Wir werden Reduktionsregeln definieren, die den Nachweis der Bedienbarkeit in den reduzierten Graphen erhalten. Die in dieser Arbeit entwickelten Algorithmen sind implementiert und in Wombat4ws, einem Analysewerkzeug f�r Web-Services, integriert worden.

Stephan Wei�leder. Semantische Fundierung der Web-Service-Beschreibungssprache WSCI. Diplomarbeit, Humboldt-Universit�t zu Berlin, November 2004.

Abstract: Wir besch�ftigen uns in dieser Arbeit mit verschiedenen Beschreibungsm�glichkeiten f�r Web Services. Im Vordergrund stehen dabei die Web-Service-Beschreibungssprache WSCI und ihre Eigenschaften. Wir werden eine Semantik entwickeln, die St�rken und Schw�chen der zugrunde liegenden Spezifikation [AAF+02] aufzeigt und mit deren Hilfe wir die Eigenschaften von WSCI �berpr�fen k�nnen.

Dirk Hain and Christian Stahl. Komposition von Web Services. Studienarbeit, Humboldt-Universit�t zu Berlin, April 2003.

Abstract: Verteilte Systeme haben in den letzten Jahren in der Informatik immer mehr an Bedeutung gewonnen. Die Web-Service-Architektur ist eine Software-Architektur zur Modellierung und Implementierung verteilter Systeme. Sie ist als eine der zukunftstr�chtigsten Technologien angesehen, die aber noch in der Erprobungsphase steckt. Unter anderem ist die Kompatibilit�t von Web Services eine offene Frage, wobei weniger syntaktische als vielmehr sematischen Kompatibilit�t problematisch ist. Diese Arbeit soll Ans�tze zur Bestimmung semantischer Kompatibilit�t von Web Services liefern.

Lars M�nzberg. Komposition von Web Services. Studienarbeit, Humboldt-Universit�t zu Berlin, June 2003.

Abstract: Verteilte Systeme haben im letzten Jahrzehnt stetig an Bedeutung gewonnen, so sind sie aus dem t�glichen Leben nicht mehr weg zu denken. Ein Beispiel hierf�r ist das Bezahlen mit der EC-Karte oder die Buchbestellung �ber das Internet. Die Web-Service-Softwarearchitektur soll die Grundlage einer neuen zukunftstr�chtigen Generation verteilter Systeme bilden. Momentan befindet sich die Technologie aber noch in der Entwicklungsphase, unter anderem ist die Komponierbarkeit von Web Services eine offene Frage. In dieser Arbeit soll ein Ansatz zur Entscheidung der als problematisch geltenden semantischen Kompatibilit�t entworfen werden.

Wolf Richter. Syntaktische Erkennung von Modellierungsfehlern in Web Services. Studienarbeit, Humboldt-Universit�t zu Berlin, December 2001.

zur�ck zur �bersicht

Theorie der Programmierung | Kontakt | XHTML 1.0 | Thu Feb 18 13:30:02 2010