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.

Quyet T.H., Thi Q.P., Hoang D.B.

72.pdf    Gửi cho bạn bè

Từ khóa : BPEL; Business Process; Control flow graphs; Control graphs; Model checker; Primary task; PROMELA; Service compositions; Service Oriented Systems; Software verification; SPIN; Spin models; Verification process; Web service composition; Information technology; Quality of service; Web services; Model checking