A formal model for BPEL4WS description of Web service composition
Xiwu Gu, LU Zheng-ding · Wuhan University Journal of Natural Sciences · 2006
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 compositiob with CSP. A set of rules for translating composition constructor of Business Process Execution Language for Web Services (BPELAWS) 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.