采用函数式语言的BPEL模型形式化验证方法

Formal Method for Verifying BPEL Model Used by Functional Programming Languag

通信顺序进程(communicating sequential process,CSP)是一种经典的形式化方法,CSP_M是在CSP基础上提出的一种函数式语言。目前Web服务组合中BPEL(business process execution language)模型缺乏可执行的形式化编程语言,通过CSP_M提出了一种基于函数式语言的BPEL模型验证方法。首先给出了基于CSP_M的BPEL模型建模与验证框架;其次给出了CSP_M的进程代数定义;再次详细描述了BPEL语言到CSP以及CSP_M的映射方法;最后以一个在线购物系统为例,讨论了该方法的使用效果。实验表明该方法可以提高BPEL模型的可靠性。

Communicating sequential process(CSP) is a classical formal method, and CSP_M is a functional programming language which is designed on the basis of CSP. Aiming at the problem that the business process execution language(BPEL) model lacks the executable formalized programming language in Web services, this paper proposes a method for verifying BPEL model based on CSP_M . Firstly, a framework is defined to model and verify BPEL model based on CSP_M . Then, the basis of CSP_M is given based on the definition of CSP. Thirdly, the mapping from BPEL to CSP and CSP_M is described. Lastly, the effect of this method is evaluated by modeling and verifying an online shopping system. The experimental results show that this method can greatly increase the reliability of BPEL model.