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.
Automatic Analysis of Control Flow in Web Services Composition Processes
MOSCATO, Francesco
2007
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
