Publikationen zum Fachbereich BPEL-Semantik

Publikationen in Zeitschriften und B�chern

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.

Konferenzbeitr�ge und Beitr�ge auf Workshops

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

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.

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

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.

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

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.

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.

zur�ck zur �bersicht

Theorie der Programmierung | Kontakt | XHTML 1.0 | Fri Sep 11 16:30:32 2009