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

pattern for the <scope> activity
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.
Download
- Paper (PDF-Dokument, 15 Seiten, 428 KB)
Links
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. Springer-Verlag, 2008.

proposed tool chain to analyze BPEL4Chor choreographies
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.
Download
- Paper (PDF-Dokument, 15 Seiten, 336 KB)
Links
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. Springer-Verlag, 2008.

an accordance-preserving transformation rule
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 transformation rules.
Download
- Paper (PDF-Dokument, 15 Seiten, 556 KB)
Links
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. Special theme on Service-Oriented Computing.

examples for ill-designed services
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.
Links
letzte Kommentare