Verification of transaction-aware web services composition through formal methods

Due to the popularity of web-based technologies and the cloud computing paradigm, organizations are adopting web services composition for the cost-effective development of business applications. Web services involved in composition can execute long-running transactions. Ensuring reliability in the execution of transaction-aware web services composition is a critical issue. Formal methods based approaches are helpful to model and verify the behaviour of web services composition before its development. This paper proposes a verification approach that presents mapping between BPEL and CSP constructs, and checks different assertions to get correct CSP and BPEL models. The proposed approach also verifies the transactional behaviour of web services composition. We have used failures-divergences refinement and new symbolic model checker tools for experiments that show the usefulness of our approach.