摘要:本发明公开了一种基于Pi演算的分布式流程验证系统,至少包括如下模块:BPEL语言编辑模块,BPEL语言到Pi演算的转换模块;Pi演算编辑模块;Pi演算验证模块;死锁原因显示模块,所述BPEL语言编辑模块、BPEL语言到Pi演算的转换模块、Pi演算编辑模块、Pi演算验证模块和死锁原因显示模块依次相连接。本发明的验证方法:用BPEL语言描述将要部署的流程;对用BPEL语言描述的流程进行转换,得到若干个Pi演算流程;对得到的Pi演算流程进行改写;采用Pi演算的规约理论进行死锁检查;用文本文件解释死锁状态。本发明可以验证用BPEL语言描述的分布式流程是否存在死锁,并精确定位死锁位置,保证在把流程部署到真实环境之后,流程运行的正确性。
- 专利类型发明专利
- 申请人西北大学;
- 发明人郭小群;侯红;丁剑洁;
- 地址710127 陕西省西安市长安区学府大道1号
- 申请号CN201010609285.0
- 申请时间2010年12月28日
- 申请公布号CN102043681A
- 申请公布时间2011年05月04日
- 分类号G06F11/00(2006.01)I;