Abstract:
The paper presents an auto-mapping method from business process execution language for Web Services (BPEL4WS) to π-calculus, checks the deadlocks property of the system expressing by π-calculus using the mobility workbench (MWB) and illustrates the approach.
Key words:
Business process execution language for Web services (BPEL4WS),
π-calculus,
Mobility workbench (MWB),
Deadlock checking
摘要： 描述了将Web服务业务流程执行语言(BPEL4WS)映射到π-演算的自动映射方法，对得到的π-演算表达式利用移动工作台（MWB）进行死锁验证，并给出一个具体示例。
关键词:
Web服务的业务流程执行语言,
π-演算,
移动工作台,
死锁验证
SONG Yan; GAO Chunming. Deadlock Checking of BPEL4WS Based on Mobility Workbench[J]. Computer Engineering, 2007, 33(01): 92-94.
宋 艳;高春鸣. 基于移动工作台的BPEL4WS死锁验证[J]. 计算机工程, 2007, 33(01): 92-94.