|
|||||
|
|
| 采用函数式语言的BPEL模型形式化验证方法 | |
| 作者单位： | ;1.南京航空航天大学计算机科学与技术学院;2.江苏师范大学计算机科学与技术学院 |
| 摘 要： | 通信顺序进程(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模型的可靠性。 |
| 关 键 词： | 函数式语言 通信顺序进程(CSP) 业务流程执行语言(BPEL) 形式化验证 模型检测 |
Formal Method for Verifying BPEL Model Used by Functional Programming Languag |
|
| Abstract: | |
| Keywords: | |