Pi演算建模BPEL4WS程序及实例研究

Modeling BPEL4WS Program with Pi Calculus and Case Study

通过对pi演算进行扩充以形式化描述BPEL4WS程序,给出了扩充pi演算的语法和操作语义,并用pi演算的通讯并发结构表示BPEL4WS规范的link结构。基于对BPEL4WS规范死路排除DPE模式的分析,提出了一个完善的解决DPE问题的pi演算形式化方法。在以上工作的基础上,系统地完成从Web服务组合语言BPEL4WS规范到扩展pi演算的映射,提出了几种验证程序性质的思路。最后给出了一个完整的案例,说明BPEL4WS程序的pi演算描述。

This paper expands the Pi calculus in order to address a formalized description of the BPEIAWS program. Moreover, it presents the grammar and manipulating semantic of expanding the Pi calculus and make use of the concurrent communication structure to represent the normative “link” structure of BPE1AWS. According to the analysis of the Dead - Path - Elimination （DPE） pattern of the BPEIAWS, a method which solves this problem of DPE by Pi calculus is proposed. Based on the above research, this paper systematically completes the mapping from Web service combination language BPEIAWS standard to the expanded Pi calculus and proposes several points of view that prove the properties of programs. At the end of this paper, a complete case is given to explain how to express BPEIAWS by the Pi calculation.