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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alves, A., et al.: Web Services Business Process Execution Language Version 2.0. Technical report, OASIS (2007)
Decker, G., Kopp, O., Leymann, F., Weske, M.: BPEL4Chor: Extending BPEL for modeling choreographies. In: 007 IEEE International Conference on Web Services (ICWS 2007), Salt Lake City, Utah, USA, July 9-13, 2007, pp. 296–303. IEEE Computer Society Press, Los Alamitos (2007)
Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting BPEL processes. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 17–32. Springer, Heidelberg (2006)
Lohmann, N., Massuthe, P., Stahl, C., Weinberg, D.: Analyzing interacting WS-BPEL processes using flexible model generation. Data Knowl. Eng. 64(1), 38–54 (2008)
Chinnici, R., Gudgin, M., Moreau, J.J., Weerawarana, S.: Web services description language (WSDL) version 1.2 part 1: Core language. World Wide Web Consortium, Working Draft WD-wsdl12-20030611 (2003)
OMG: Business Process Modeling Notation (BPMN) Specification. Final Adopted Specification, Object Management Group (2006), http://www.bpmn.org
Massuthe, P., Reisig, W., Schmidt, K.: An operating guideline approach to the SOA. Annals of Mathematics, Computing & Teleinformatics 1(3), 35–43 (2005)
van der Aalst, W.M.P.: The application of Petri nets to workflow management. Journal of Circuits, Systems and Computers 8(1), 21–66 (1998)
Schmidt, K.: Controllability of open workflow nets. In: Desel, J., Frank, U. (eds.) Enterprise Modelling and Information Systems Architectures, Proceedings of the Workshop in Klagenfurt, October 24-25, 2005. Lecture Notes in Informatics (LNI), vol. 75, pp. 236–249 (2005)
Breugel, F.v., Koshkina, M.: Models and verification of BPEL (2006), http://www.cse.yorku.ca/~franck/research/drafts/tutorial.pdf
Lohmann, N.: A feature-complete Petri net semantics for WS-BPEL 2.0. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol. 4937, pp. 77–91. Springer, Heidelberg (2007)
Schmidt, K.: LoLA: A low level analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 465–474. Springer, Heidelberg (2000)
Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Petrify: A tool for manipulating concurrent specifications and synthesis of asynchronous controllers. Trans. Inf. and Syst. E80-D(3), 315–325 (1997)
Lassen, K.B., van der Aalst, W.M.P.: WorkflowNet2BPEL4WS: A tool for translating unstructured workflow processes to readable BPEL. In: Meersman, R., Tari, Z. (eds.) OTM 2006. LNCS, vol. 4275, pp. 127–144. Springer, Heidelberg (2006)
Lohmann, N., Massuthe, P., Wolf, K.: Behavioral constraints for services. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 271–287. Springer, Heidelberg (2007)
Decker, G., Kopp, O., Puhlmann, F.: Service referrals in BPEL-based choreographies. In: 2nd European Young Researchers Workshop on Service Oriented Computing (YR-SOC 2007), pp. 25–30. University of Leicester (2007)
Zaha, J.M., Barros, A., Dumas, M., ter Hofstede, A.: Let’s dance: A language for service behavior modeling. In: Meersman, R., Tari, Z. (eds.) OTM 2006. LNCS, vol. 4275, pp. 145–162. Springer, Heidelberg (2006)
Kavantzas, N., Burdett, D., Ritzinger, G., Lafon, Y.: Web Services Choreography Description Language Version 1.0. W3C Candidate Recommendation, W3C (2005), http://www.w3.org/TR/ws-cdl-10
Decker, G., Zaha, J.M., Dumas, M.: Execution semantics for service choreographies. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 163–177. Springer, Heidelberg (2006)
Busi, N., Gorrieri, R., Guidi, C., Lucchi, R., Zavattaro, G.: Choreography and orchestration conformance for system design. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 63–81. Springer, Heidelberg (2006)
Corredini, F., De Angelis, A.P.: Verification of WS-CDL choreographies. In: 2nd European Young Researchers Workshop on Service Oriented Computing (YR-SOC 2007), pp. 13–18. University of Leicester (2007)
Puhlmann, F., Weske, M.: Investigations on soundness regarding lazy activities. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 145–160. Springer, Heidelberg (2006)
Moser, S., Martens, A., Häbich, M., Mülle, J.: A hybrid approach for generating compatible WS-BPEL partner processes. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 458–464. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lohmann, N., Kopp, O., Leymann, F., Reisig, W. (2008). Analyzing BPEL4Chor: Verification and Participant Synthesis. In: Dumas, M., Heckel, R. (eds) Web Services and Formal Methods. WS-FM 2007. Lecture Notes in Computer Science, vol 4937. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79230-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-79230-7_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79229-1
Online ISBN: 978-3-540-79230-7
eBook Packages: Computer ScienceComputer Science (R0)