Abstract: Communicating sequential process (CSP) is a classical formal method, and CSPM 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 CSPM. Firstly, a framework is defined to model and verify BPEL model based on CSPM. Then, the basis of CSPM is given based on the definition of CSP. Thirdly, the mapping from BPEL to CSP and CSPM 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.

Key words: functional programming language, communicating sequential process (CSP), business process execution language (BPEL), formal verification, model checking

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

关键词: 函数式语言, 通信顺序进程（CSP）, 业务流程执行语言（BPEL）, 形式化验证, 模型检测