FORMAL ANALYSIS OF WEB SERVICES COMPOSITION

Web services composition is an emerging paradigm for defining complex web services from standard web services.  The Web Services Business Process Execution Language (WS-BPEL) is the standard for specifying and executing workflow specification for web service composition.  As with any system that supports complex constructs such as currency, testing approach alone is not an effective method for detecting faults.  Hence there is a growing interest in formal modeling, analysis and verification of WS-BPEL in order to detect bugs, ensure correctness of desired properties among others.  Also maintaining a system of complex business processes with multiple business partners can be quite cumbersome.  Program slicing as a static analysis technique can be used in acquiring better understanding of a program.  In this paper, we provide an overview of program slicing, formal methods (model checking, theorem proveers) and formal analysis techniques that have been applied to WS-BPEL over the years.