A Formal Model for BPEL4WS Description of Web Service Composition

摘要

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 compositionconstructor of Business Process Execution Language for Web Services (BPEL4WS) 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 formodel checking, model verification and model simulation are also introduced.