Advanced verification of distributed WS-BPEL business processes incorporating CSSA-based data flow analysis. (13th July 2009)

• Record Type: Journal Article
• Authors: Amme, Wolfram; Martens, Axel; Moser, Simon
• Is Part Of: International journal of business process integration and management. Volume 4:Number 1(2009)
• Page Start: 47
• Page End: 59
• Publication Date: 2009-07-13
• Subjects: SOA -- business process execution language -- web services -- WS-BPEL -- concurrent single static assignment -- CSSA -- formal verification -- data flow analysis -- Petri nets -- service compatibility -- business process integration -- business process management -- BPEL; Business -- Computer networks -- Periodicals; Industrial management -- Periodicals; 658.054605
• Languages: English
• ISSNs: 1741-8763

Abstract

The business process execution language for web services (WS-BPEL) provides a technology to aggregate encapsulated functionalities for defining high-value web services. For a distributed application in a B2B interaction, the partners simply need to expose their provided functionality as BPEL processes and compose them. Verifying such distributed web service based systems has been a huge topic in the research community lately. However, in most of the work on analysing properties of interacting web services, especially when backed by stateful implementations like WS-BPEL, the data flow present in the implementation is widely neglected and the analysis focuses on control flow only. This might lead to false-positive analysis results when searching for design weaknesses and errors of a given BPEL process. In this paper, we present a method to extract data flow information by constructing a CSSA representation and detecting data dependencies that effect communication behaviour. Those discovered dependencies are used to construct a more precise formal model of the given BPEL process and hence to improve the quality of analysis results.