A method of verifying web service composition
Service composition is one of the primary tasks in developing service-oriented systems. However, there are currently some challenges to check its correction. In this paper, we propose a visual methodology and a tool for verifying business processes written in BPEL by using the SPIN model checker. We present algorithms to translate BPEL processes into PROMELA programs via labeled control flow graphs. The use of label control graphs in the tool will help regular users understand BPEL business processes and the verification process with a model checker more easily. Finally, the Spin model checker will verify important properties of the PROMELA program that represents a BPEL business process. © 2010 ACM.