TY - GEN
T1 - Modeling and verifying web services choreography using process algebra
AU - Li, Jing
AU - He, Jifeng
AU - Zhu, Huibiao
AU - Pu, Geguang
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/47749095956
U2 - 10.1109/SEW.2007.105
DO - 10.1109/SEW.2007.105
M3 - 会议稿件
AN - SCOPUS:47749095956
SN - 0769528627
SN - 9780769528625
T3 - Proceedings - International Conference on Software Engineering
SP - 256
EP - 265
BT - 31st Annual IEEE Software Engineering Workshop, SEW-31 2007 - Proceedings
T2 - 31st Annual IEEE Software Engineering Workshop, SEW-31 2007
Y2 - 6 March 2007 through 8 March 2007
ER -