Verification of Service Composition and Compensation by Using Process Algebra
Shamim Ripon · Journal of Advances in Computer Networks · 2016
Web service technology provides a platform that facilitates the development of distributed services.In order to support business to business interactions within the distributed environment a crying need is to aggregate web services and assemble them is a goal oriented infrastructure.With the emergence of web services, the coordination and interaction involved between multiple business partners are conducted by using the web services.Faults can arise at any stage of business transaction and handling such faults where multiple partners are involved is both crucial and difficult.Process algebras can be used to model concurrent and distributed interactive systems.Compensating CSP is a language defined to model business transactions within the framework of CSP process algebra.It has the facility to model faults within a transaction as compensations.However, the language lacks automated tool support to verify the service composition.Finite state Process (FSP), on the other hand, is designed to model the composition of web services and importantly, it has an automated tool support for verification of composition of services, however there is no construct for compensation.By combining the benefits the both cCSP and FSP, this paper illustrates a mechanism to model and verify the composition of services and compensation in FSP by following the mechanism adopted in cCSP.The verification of composition properties is performed by LTSA tool.