Model checking web services choreography in process analysis toolkit

Web service(WS) is an emerging software technology,especially acting an important role in cloud computing.The WS choreography description language(WS-CDL) is the standard for modeling the observable behavior of WS composition across multiple participants from a global point of view.However,it lacks of a formal semantics and could easily lead to misunderstanding and different implementations.In this paper,the WS-CDL based specifications are formally extracted in a communicating sequential process supporting a formal approach to checking WS models.In addition,formalisms and model checking are explicitly illustrated through a simple but non-trivial example with the help of model checker process analysis toolkit(PAT).