It is now well-admitted that formal methods are helpful for many issues raised in the Web services
area. It is a feasible method of the design and the verification of Web services using process algebras.
BPEL4WE can correctly combine Web services actions. It is a important part of Web Services. In this paper,
we present a mapping from BPEL4WS code to value-passing CCS, which offer an available way of obtaining a
formal model of BPEL4WS.