Automata Semantics and Analysis ofBPEL

Abstract-Web service is an emerging paradigm for distrib-uted computing. In order to verify web services rigorously, it is important to provide a formal semantics for flow-based web service languages such as BPEL. A suitable formal model should cover most features of BPEL. The existing formal mod-els either abstract from data, cover a simple subset of BPEL, or omit the interactions between BPEL activities. This paper presents Web Service Automata, an extension of Mealy ma-chines, to fulfil the formal model requirements of the web ser-vice domain. Secondly, the paper analyses the control handling and data handling of BPEL, so that these can be verified in a clear manner. Index Terms- Web service, BPEL, finite state machine, de-sign model analysis. I