首页|Model checking web services choreography in process analysis toolkit
Model checking web services choreography in process analysis toolkit
扫码查看
点击上方二维码区域,可以放大扫码查看
原文链接
NETL
NSTL
万方数据
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).
model checkingweb service (WS)communicating sequential processes (CSP)
XU Dong、LEI Zhou、LI Wei-min、ZHANG Bo-feng
展开 >
School of Computer Engineering and Science,Shanghai University,Shanghai 200072,P.R.China
High Performance Computing Center,Shanghai University,Shanghai 200072,P.R.China