Title :
Automata Semantics and Analysis of BPEL
Author :
Zheng, Yongyan ; Krause, Paul
Author_Institution :
Surrey Univ., Guildford
Abstract :
Web service is an emerging paradigm for distributed 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 models 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 machines, to fulfil the formal model requirements of the web service domain. Secondly, the paper analyses the control handling and data handling of BPEL, so that these can be verified in a clear manner.
Keywords :
Web services; data handling; finite state machines; formal languages; formal verification; BPEL analysis; Mealy machines; Web service; automata semantics; business process execution language; control handling; data handling; distributed computing; finite state machine; formal model; formal semantics; Automata; Automatic control; Computer architecture; Data analysis; Data handling; Distributed computing; Ecosystems; Message passing; Testing; Web services; BPEL; Web service; design model analysis; finite state machine;
Conference_Titel :
Digital EcoSystems and Technologies Conference, 2007. DEST '07. Inaugural IEEE-IES
Conference_Location :
Cairns
Print_ISBN :
1-4244-0470-3
Electronic_ISBN :
1-4244-0470-3
DOI :
10.1109/DEST.2007.371961
