Modeling and Verifying Web Services Choreography Using Process Algebra Export

@inproceedings{citeulike:2578312, abstract = {The Web Services Choreography Description Language (WS-CDL) is a newly developed specification for web services composition to describe the observable behav- ior across multiple participants from a global perspective. However, this specification does not provide a formal se- mantics, whose informal description can lead to ambigu- ous understanding and different implementations. Hence, it causes difficulties for the engineering community to an- alyze 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 de- signing and verifying concurrent processes. Therefore, all the properties we want to check within a WS-CDL docu- ment can be verified automatically in the CSP framework correspondingly. In addition, the exception and compen- sation handling mechanism, an important concept of long running transactions, is demonstrated clearly through our formalization work.}, author = {Li, Jing and He, Jifeng and Zhu, Huibiao and Pu, Geguang}, booktitle = {Software Engineering Workshop, 2007. SEW 2007. 31st IEEE}, citeulike-article-id = {2578312}, citeulike-linkout-0 = {http://dx.doi.org/10.1109/SEW.2007.105}, citeulike-linkout-1 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4402784}, comment = {cited Lucchi's paper, maybe some dynamic properties were handled.}, doi = {10.1109/SEW.2007.105}, journal = {Software Engineering Workshop, 2007. SEW 2007. 31st IEEE}, keywords = {choreography, csp, verification}, pages = {256--268}, posted-at = {2008-03-24 05:01:57}, priority = {2}, title = {Modeling and Verifying Web Services Choreography Using Process Algebra}, url = {http://dx.doi.org/10.1109/SEW.2007.105}, year = {2007} }

TY - CONF ID - citeulike:2578312 L3 - citeulike-article-id:2578312 N2 - The Web Services Choreography Description Language (WS-CDL) is a newly developed specification for web services composition to describe the observable behav- ior across multiple participants from a global perspective. However, this specification does not provide a formal se- mantics, whose informal description can lead to ambigu- ous understanding and different implementations. Hence, it causes difficulties for the engineering community to an- alyze 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 de- signing and verifying concurrent processes. Therefore, all the properties we want to check within a WS-CDL docu- ment can be verified automatically in the CSP framework correspondingly. In addition, the exception and compen- sation handling mechanism, an important concept of long running transactions, is demonstrated clearly through our formalization work. JF - Software Engineering Workshop, 2007. SEW 2007. 31st IEEE EP - 268 TI - Modeling and Verifying Web Services Choreography Using Process Algebra T2 - Software Engineering Workshop, 2007. SEW 2007. 31st IEEE SP - 256 KW - choreography KW - csp KW - verification N1 - cited Lucchi's paper, maybe some dynamic properties were handled. AU - Li, Jing AU - He, Jifeng AU - Zhu, Huibiao AU - Pu, Geguang PY - 2007/// UR - http://dx.doi.org/10.1109/SEW.2007.105 ER -