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

来源：计算机科学与探索杂志2018年第2期北京时间：

作者：祝义，黄志球，周航

单位：1. 南京航空航天大学 计算机科学与技术学院，南京 210016 2. 江苏师范大学 计算机科学与技术学院，江苏 徐州 221116

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

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