Formal semantics and analysis of control flow in WS-BPEL
Chun Ouyang, Wil M. P. van der Aalst, Stephan Breutel, Marlon Dumas, Arthur H. M. ter Hofstede, H. M. W. Verbeek · QUT ePrints (Queensland University of Technology) · 2005
Abstract. Web service composition refers to the creation of new (Web) services by combination of functionality provided by existing ones. This paradigm has gained signi¯cant attention in the Web services community and is seen as a pillar for building service-oriented applications. A number of domain-speci¯c languages for service composition have been proposed with consensus being formed around a process-oriented language known as WS-BPEL (or BPEL). The kernel of BPEL consists of simple communication primitives that may be combined using control-°ow constructs expressing sequence, branching, parallelism, synchronisation, etc. As a result, BPEL process de¯nitions lend themselves to static °ow-based analysis techniques. In this report, we describe a tool that performs two useful types of static checks and extracts meta-data to optimise dynamic resource management. The tool operates by translating BPEL processes into Petri nets and exploiting existing Petri net analysis techniques. It relies on a comprehensive and rigorously de¯ned mapping of BPEL constructs into Petri net structures.