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

摘要

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

主权项

一种基于Pi演算的分布式流程验证系统，其特征在于，所述的验证系统至少包括如下模块：BPEL语言编辑模块，用来开发被验证的BPEL流程；BPEL语言到Pi演算的转换模块，用来将被开发出来的BPEL流程转换为Pi演算；Pi演算编辑模块，用来对转换后的Pi演算进行改写；Pi演算验证模块，用来对生成的Pi演算公式进行验证：把转换后的每个Pi演算公式当作一个进程，然后将所有进程共同推进，通过进程间的通信判断是否有流程死锁发生；死锁原因显示模块，用来显示解释死锁状态的文本文件；所述BPEL语言编辑模块、BPEL语言到Pi演算的转换模块、Pi演算编辑模块、Pi演算验证模块和死锁原因显示模块依次相连接，在Pi演算验证模块中，通过各模块互相之间的进程通信来判断分布式流程中是否存在死锁，并在死锁原因显示模块中通过显示解释死锁状态的文本文件来定位死锁位置。