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. ACM, April 2008.
relationship between syntactic compatibility and behavioral equivalence
Abstract. WS-BPEL defines a standard for executable 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 exist 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 and Jens Kleine. Fully-automatic translation of open workflow net models into simple 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. GI, March 2008.
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. 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.
link wrapper pattern
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].
Download
- Paper (PDF-Dokument, 41 Seiten, 1447 KB)
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
letzte Kommentare