×

A formal model for BPEL4WS description of web service composition. (English) Zbl 1115.68306

Summary: Communicating Sequential Processes (CSP) is a kind of process algebra, which is suitable for modeling and verifying Web service composition. This paper describes how to model Web service composition with CSP. A set of rules for translating composition constructor of business process execution language for web services to CSP notations is defined. According to the rules that have been defined, the corresponding translation algorithm is designed and illustrated with examples. The methods for model checking, model verification and model simulation are also introduced.

MSC:

68M10 Network design and communication in computer systems

Software:

CCSP
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Andrews T, Curbera F, Dholakia H,et al. Business Process Execution Language for Web Services Versionl. 1 [EB/OL]. [2003-05-05].http://www128.ibm.com/developerworks/library/specification/ws-bpel/.
[2] Leymann F. Web Services Flow Language (WSFL1.0) [EB/OL]. [2005-10-20].http://www306.ibm.com/software/solutions/Webservices/pdf/WSFL.pdf.
[3] Hamadi R, Benatallah B. A Petri Net-based Model for Web Service Composition [C]//Database Technologies 2003, Proc of Fourteenth Australasian Database Conference (ADC2003). Sydney: Australian Computer Society, 2003: 191–200.
[4] Van der Aalst W M P, ter Hofstede A H M. Verification of Workflow Task Structures: A Petri-Net-Based Approach [J].Information Systems, 2000,25(1): 43–69. · Zbl 0956.68521
[5] Rao Jinghai.Semantic Web Service. Composition via. Logic-Based Program. Synthesis [D]. N-7491 Trondheim: Department of Computer and Information Science, Norwegian University of Science and Technology, 2004.
[6] Lumpe M.A Pi-Calculus Based Approach to Software Composition [D]. Switzerland: Institute of Computer Science and Applied Mathematics, University of Bern, 1999.
[7] Hoare C A R.Communicating Sequential Processes [M]. New Jersey: Prentice-Hall, 2004. · Zbl 0383.68028
[8] Hoare C A R. Communicating Sequential Processes [J].Communications of the ACM, 1978,21(8): 666–677. · Zbl 0383.68028
[9] Wohed P, van der Aalst W M P, Dumas M,et al. Pattern Based Analysis of BPEL4WS [R]. Queensland: Queensland University of Technology, 2004.
[10] Foster H, Uchitel S, Magee J,et al. Model-Based Verification of Web Service Compositions [C]//Proceedings of the 18th IEEE International Conference on Automated Software Engineering. Montreal, Canada: IEEE Computer Society Press, 2003: 152–161.
[11] Roscoe A W.The Theory and Practice of Concurrency [M]. New Jersey: Prentice-Hall, 1997.
[12] Lutfiyya H, Mc Millin B, Arrowsmith B,et al. CCSP–A Formal System for Distributed Program Debugging [R]. Rolla, New Jersey: University of Missouri, 1994.
[13] Welch P, Austin P. CSP for Java (JCSP) [EB/OL]. [2005-11-05].http://www.cs.kent.ac.uk/projects/ofa/jcsp/explain.html.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.