基于Pi演算的分布式流程验证系统及方法

摘要

本发明公开了一种基于Pi演算的分布式流程验证系统，至少包括如下模块：BPEL语言编辑模块，BPEL语言到Pi演算的转换模块；Pi演算编辑模块；Pi演算验证模块；死锁原因显示模块，所述BPEL语言编辑模块、BPEL语言到Pi演算的转换模块、Pi演算编辑模块、Pi演算验证模块和死锁原因显示模块依次相连接。本发明的验证方法：用BPEL语言描述将要部署的流程；对用BPEL语言描述的流程进行转换，得到若干个Pi演算流程；对得到的Pi演算流程进行改写；采用Pi演算的规约理论进行死锁检查；用文本文件解释死锁状态。本发明可以验证用BPEL语言描述的分布式流程是否存在死锁，并精确定位死锁位置，保证在把流程部署到真实环境之后，流程运行的正确性。