Artikel in Tagungsband INPROC-2007-81

Lohmann, Niels; Kopp, Oliver; Leymann, Frank; Reisig, Wolfgang: Analyzing BPEL4Chor: Verification and Participant Synthesis.
In: Dumas, Marlon (Hrsg); Heckel, Reiko (Hrsg): Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia.
Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik.
S. 46-60, englisch.
Springer-Verlag, 28. September 2007.
DOI: 10.1007/978-3-540-79230-7_4.
Artikel in Tagungsband (Workshop-Beitrag).
CR-Klassif.D.2.4 (Software Engineering Software/Program Verification)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
F.3.2 (Semantics of Programming Languages)
K.1 (The Computer Industry)

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

Volltext und
andere Links
WS-FM 2007
Abteilung(en)Universität Stuttgart, Institut für Architektur von Anwendungssystemen
Eingabedatum14. März 2008
   Publ. Institut   Publ. Informatik