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

摘要：

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

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

所属期刊栏目：12

分类号：TP311(计算技术、计算机技术)

资助基金：The National Natural Science Foundation of China under Grant No.61502212;the Postdoctoral Science Foundation of Jiangsu Province under Grant No.1501055B

在线出版日期：2018-04-04（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：185-196