Publikationen zum Fachbereich BPEL

Publikationen in Zeitschriften und Büchern

• Niels Lohmann, Eric Verbeek, and Remco Dijkman. Petri Net Transformations for Business Processes -- A Survey. Transactions on Petri Nets and Other Models of Concurrency II, Special Issue on Concurrency in Process-Aware Information Systems, 2: 46-63, March 2009.

  Abstract: In Process-Aware Information Systems, business processes are often modeled in an explicit way. Roughly spoken, the available business process modeling languages can be divided into two groups. Languages from the first group are preferred by academic people but shunned by business people, and include Petri nets and process algebras. These academic languages have a proper formal semantics, which allows the corresponding academic models to be verified in a formal way. Languages from the second group are preferred by business people but disliked by academic people, and include BPEL, BPMN, and EPCs. These business languages often lack any proper semantics, which often leads to debates on how to interpret certain business models. Nevertheless, business models are used in practice, whereas academic models are hardly used. To be able to use, for example, the abundance of Petri net verification techniques on business models, we need to be able to transform these models to Petri nets. In this paper, we investigate a number of Petri net transformations that already exist. For every transformation, we investigate the transformation itself, the constructs in the business models that are problematic for the transformation and the main applications for the transformation.

  

• 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.

  

• Niels Lohmann, Eric Verbeek, Chun Ouyang, and Christian Stahl. Comparing and Evaluating Petri Net Semantics for BPEL. IJBPIM, 2008. Note: (Accepted for publication).

  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.

  

• 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.

  

Konferenzbeiträge und Beiträge auf Workshops

• Dirk Fahland, Daniel Lübke, Jan Mendling, Hajo Reijers, Barbara Weber, Matthias Weidlich, and Stefan Zugal. Declarative versus Imperative Process Modeling Languages: The Issue of Understandability. In John Krogstie, Terry Halpin, and Erik Proper, editors, Proceedings of the 14th International Conference on Exploring Modeling Methods in Systems Analysis and Design (EMMSAD'09), volume 29 of Lecture Notes in Business Information Processing, Amsterdam, The Netherlands, pages 353-366, June 2009. Springer-Verlag. Note: (to appear).

  Abstract: Advantages and shortcomings of different process modeling languages are heavily debated, both in academia and industry, but little evidence is presented to support judgements. With this paper we aim to contribute to a more rigorous, theoretical discussion of the topic by drawing a link to well-established research on program comprehension. In particular, we focus on imperative and declarative techniques of modeling a process. Cognitive research has demonstrated that imperative programs deliver sequential information much better while declarative programs offer clear insight into circumstantial information. In this paper we show that in principle this argument can be transferred to respective features of process modeling languages. Our contribution is a pair of propositions that are routed in the cognitive dimensions framework. In future research, we aim to challenge these propositions by an experiment.

  

• 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, 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.

  

• Dieter König, Niels Lohmann, Simon Moser, Christian Stahl, and Karsten Wolf. Extending the Compatibility Notion for Abstract WS-BPEL Processes. In Wei-Ying Ma, Andrew Tomkins, and Xiaodong Zhang, editors, Proceedings of the 17th International Conference on World Wide Web, WWW 2008, Beijing, China, April 21--25, 2008, pages 785-794, April 2008. ACM.

  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. 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 77-91, 2008. Springer-Verlag.

  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 and Jens Kleine. Fully-automatic Translation of Open Workflow Net Models into Human-readable Abstract BPEL Processes. In Thomas Kühne, Wolfgang Reisig, and Friedrich Steimann, editors, Modellierung 2008, 12.-14. März 2008, Berlin, Proceedings, volume P-127 of Lecture Notes in Informatics (LNI), pages 57-72, March 2008. GI.

  Abstract: On the one hand, Petri net models have a successful history in the modeling, simulation, and verification of workflows and business processes. On the other hand, BPEL is the de facto standard for describing executable Web service-based business processes. With abstract BPEL processes, BPEL can also be used as modeling language. However, being a complicated language with many syntactic constraints, abstract BPEL processes impede a straightforward modeling. In this paper, we introduce a fully-automatic translation of Petri net models into abstract BPEL processes which can be refined to executable BPEL processes. This approach combines strengths of Petri nets in modeling and verification with the ability to execute BPEL processes. Furthermore, it completes the Tools4BPEL framework to synthesize BPEL processes which are correct by design.

  

• Niels Lohmann, Oliver Kopp, Frank Leymann, and Wolfgang Reisig. Analyzing BPEL4Chor: Verification and Participant Synthesis. 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 46-60, 2008. Springer-Verlag.

  Abstract: Choreographies offer means to capture global interactions between business processes of different partners. BPEL4Chor has been introduced to describe these interactions using BPEL. Currently, there are no formal methods available to verify BPEL4Chor choreographies. In this paper, we present how BPEL4Chor choreographies can be completely verified using Petri nets. A case study undermines that our verification techniques scale. Additionally, we show how the verification techniques can be used to generate a stub process for a partner taking part in a choreography. This is especially useful when the behavior of one participant is intended to follow the corresponding requirements of the other participants. Thus, the missing participant behavior can be generated and the error-prone design of that participant can be skipped.

  

• 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.

  

• 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.

  

• 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.

  

• 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. Simulation and Equivalence between BPEL Process Models. In Proceedings of the Design, Analysis, and Simulation of Distributed Systems Symposium (DASD'05), Part of the 2005 Spring Simulation Multiconference (SpringSim'05), San Diego, California, April 2005.

  Abstract: The integration of business process across the boundaries of individual enterprises or business units is becoming increasingly important. In this scenario, process models play an all-important role. On the one hand, the interaction between the participating companies often is specified globally, for example by means of multiple abstract process models - one for each partner. On the other hand, each partner defines its local process autonomously in terms of an executable process model. The important question is whether such an executable model is consistent to the predefined abstract model. This paper defines a simulation relation between BPEL process models, and presents a method to verify consistency automatically, on top of it.

  

• 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 and Christian Stahl. A Petri net semantic for BPEL4WS - validation and application. In Ekkart Kindler, editor, Proceedings of the 11th Workshop on Algorithms and Tools for Petri Nets (AWPN'04), pages 1-6, October 2004. Universität Paderborn.

  Abstract: We translated a small business process into a recently defined Petri net semantic. Then we used the tool LoLA for validating the semantic as well as for proving relevant properties of the particular process.

  

Technische Berichte

• 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.

  

• 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.

  

• 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].

  

• 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.

  

• 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.

  

• Wolfgang Reisig, Karsten Schmidt, and Christian Stahl. Verteilte Geschäftsprozesse modellieren und analysieren. Informatik-Berichte 182, Humboldt-Universität zu Berlin, February 2005.

  Abstract: Verteilte Geschäftsprozesse nutzen das Internet, um auf heterogenen Rechnerstrukturen Dienste auszubieten. Modellierungstechniken und Implementierungssprachen für solche Dienste werfen im Vergleich mit herkömmlichen Rechnern grundlegend neue Fragestellungen auf. Wir diskutieren einige davon und zeigen, wie Petrinetze ihre Beantwortung ermöglichen.

  

• 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.

  

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.

  

• 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.

  

• 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.

  

• Sebastian Hinz. Implementierung einer Petrinetz-Semantik für BPEL. Diplomarbeit, Humboldt-Universität zu Berlin, March 2005.

  Abstract: BPEL ist eine Modellierungssprache zur Beschreibung von verteilten Geschäftsprozessen mit Webservices. Um mit formalen Methoden die Sprache selbst und in BPEL modellierte Prozesse verifizieren zu können, wird eine formale Semantik benötigt. Auf der Basis von Petrinetzen wurde bereits eine solche Semantik entwickelt. Um die Analyse eines Prozesses zu ermöglichen wird ein Werkzeug benötigt, das die Transformation des Prozesses in ein Petrinetz übernimmt. In der vorliegenden Arbeit wird ein solches Werkzeug entwickelt, vorgestellt und seine Funktionsweise erläutert.

  

• 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.

  

• Carsten Frenkler. BPEL-Boxen. Ein Modell zur Integration von Transaktionskonzepten in Geschäftsprozesse mit Petrinetzen. Studienarbeit, Humboldt-Universität zu Berlin, February 2004.

• 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.

  

• Thomas Heidinger. Statische Analyse von BPEL4WS-Prozessmodellen. Studienarbeit, Humboldt-Universität zu Berlin, December 2003.

• Daniela Weinberg. Graphische Repräsentation von BPEL. Studienarbeit, Humboldt-Universität zu Berlin, August 2003.

zurück zur Übersicht