Article in Proceedings INPROC-2007-81

BibliographyLohmann, Niels; Kopp, Oliver; Leymann, Frank; Reisig, Wolfgang: Analyzing BPEL4Chor: Verification and Participant Synthesis.
In: Dumas, Marlon (ed.); Heckel, Reiko (ed.): Web Services and Formal Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology.
pp. 46-60, english.
Springer-Verlag, September 28, 2007.
DOI: 10.1007/978-3-540-79230-7_4.
Article in Proceedings (Workshop Paper).
CR-SchemaD.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)
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 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.

Full text and
other links
WS-FM 2007
Tools4BPEL-Projektseite
Contactkopp@iaas.uni-stuttgart.de
Department(s)University of Stuttgart, Institute of Architecture of Application Systems
Project(s)Tools4BPEL
Entry dateMarch 14, 2008
   Publ. Institute   Publ. Computer Science