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

• 作者: 周航 祝义 黄志球
• 来源期刊: 计算机科学与探索
• 学科: 工学
• 关键词: 函数式语言 通信顺序进程(CSP) 业务流程执行语言(BPEL) 形式化验证 模型检测
• 年，卷（期）: 2018,（2）
• 所属期刊栏目: 学术研究
• 页码范围: 185-196
• 页数: 12页
• 分类号: TP311
• 字数: 5791字
• 语种: 中文
• DOI: 10.3778/j.issn.1673-9418.1611056

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄志球	南京航空航天大学计算机科学与技术学院	183	1755	20.0	33.0
2	祝义	南京航空航天大学计算机科学与技术学院	15	179	8.0	13.0
4	周航	南京航空航天大学计算机科学与技术学院	34	186	8.0	11.0