Web Services can be composed to build domain-specific application and solution. Some Web Services Composition (WSC) standards are proposed, for instance, WS-BPEL and WS-CDL. WS-BPEL consists of basic activity, structured activity and control-flow. It uses control-flow to construct sequence, branching, parallelism, synchronization, etc. This paper proposes an approach to formally analyze transaction behavior in WS-BPEL through General Stochastic High-level Petri Net (GSHLPN). Unlike other approaches based on Petri Net, our approach can simulate the interrupt behavior resulted from the trigger of failure and user exception operation in WS-BPEL, and accurately compute the time of process, whereas other approaches can not effectively do so.