Modeling and Verifying Web Services Choreography Using Process Algebra

1 March 2007

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

No. 15506215,p. 256-268
https://doi.org/10.1109/sew.2007.105

Abstract

The Web Services Choreography Description Language (WS-CDL) is a newly developed specification for Web services composition to describe the observable behavior across multiple participants from a global perspective. However, this specification does not provide a formal semantics, whose informal description can lead to ambiguous understanding and different implementations. Hence, it causes difficulties for the engineering community to analyze the business behavior and ensure the correctness. In this paper, we present the semantics of WS-CDL in terms of process algebra CSP which has great advantages in designing and verifying concurrent processes. Therefore, all the properties we want to check within a WS-CDL document can be verified automatically in the CSP framework correspondingly. In addition, the exception and compensation handling mechanism, an important concept of long running transactions, is demonstrated clearly through our formalization work.

Keywords

This publication has 4 references indexed in Scilit:

Towards a formal framework for Choreography
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2006
Theoretical foundations for compensations in flow composition languages
Published by Association for Computing Machinery (ACM) ,2005
Formalizing Web Service Choreographies
Electronic Notes in Theoretical Computer Science, 2004
Sagas
Published by Association for Computing Machinery (ACM) ,1987