Automata Semantics and Analysis of BPEL

Author

Zheng, Yongyan ; Krause, Paul

Author_Institution

Surrey Univ., Guildford

fYear

2007

fDate

21-23 Feb. 2007

Firstpage

147

Lastpage

152

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/DEST.2007.371961

Filename

4233695