Automatic Analysis of Control Flow inWeb Services Composition Processes

Author

Di Lorenzo, Giusy ; Moscato, Francesco ; Mazzocca, Nicola ; Vittorini, Valeria

Author_Institution

Dip. di Ing. Dell´´Informazione, Univ. di Napoli Federico II

fYear

2007

fDate

7-9 Feb. 2007

Firstpage

299

Lastpage

306

Abstract

Composition of Web services is of great interest to support business-to-business collaboration and provide value added services with desired properties or capabilities. Nevertheless, the standard languages used to create business processes from composite Web services lack of formal definition of their semantics and tools to support the analysis of a business process. In this paper we provide a practical approach to formal verification of BPEL4WS executable processes. A syntax-driven operational semantics for BPEL4WS is introduced and an automatic verifier is presented in order to perform a semantic analysis of the flow constructs used in the definition of BPEL4WS processes

Keywords

Web services; program diagnostics; program verification; programming language semantics; specification languages; BPEL4WS executable process; Web services composition; automatic analysis; automatic verification; business-to-business collaboration; control flow; formal verification; semantic analysis; syntax-driven operational semantics; Algebra; Automata; Automatic control; Collaboration; Formal verification; Performance analysis; Petri nets; Protocols; Service oriented architecture; Web services;

fLanguage

English

Publisher

ieee

Conference_Titel

Parallel, Distributed and Network-Based Processing, 2007. PDP '07. 15th EUROMICRO International Conference on

Conference_Location

Napoli

ISSN

1066-6192

Print_ISBN

0-7695-2784-1

Type

conf

DOI

10.1109/PDP.2007.27

Filename

4135290