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

doi:10.3778/j.issn.1673-9418.1611056

计算机科学与探索 ›› 2018, Vol. 12 ›› Issue (2): 185-196.DOI: 10.3778/j.issn.1673-9418.1611056

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

祝义1,2+，黄志球1，周航1

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

出版日期:2018-02-01 发布日期:2018-01-31

Formal Method for Verifying BPEL Model Used by Functional Programming Language

ZHU Yi1,2+, HUANG Zhiqiu1, ZHOU Hang1

1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
2. School of Computer Science and Technology, Jiangsu Normal University, Xuzhou, Jiangsu 221116, China

Online:2018-02-01 Published:2018-01-31

摘要/Abstract

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

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

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

祝义，黄志球，周航. 采用函数式语言的BPEL模型形式化验证方法[J]. 计算机科学与探索, 2018, 12(2): 185-196.

ZHU Yi, HUANG Zhiqiu, ZHOU Hang. Formal Method for Verifying BPEL Model Used by Functional Programming Language[J]. Journal of Frontiers of Computer Science and Technology, 2018, 12(2): 185-196.

[1]	张俊. SCVerify：抗功耗侧信道攻击软件实现的验证[J]. 计算机科学与探索, 2021, 15(6): 1074-1083.
[2]	魏杰林，袁申，李永明，梁常建. 具有DP的广义可能性模糊时态CTL模型检测[J]. 计算机科学与探索, 2019, 13(10): 1781-1792.
[3]	朱晔，袁红娟，钱俊彦，潘海玉. 模糊交互时态逻辑的一些标记[J]. 计算机科学与探索, 2018, 12(12): 2033-2040.
[4]	鱼先锋，李超，李永明. 直觉模糊测度的计算树逻辑[J]. 计算机科学与探索, 2017, 11(9): 1523-1530.
[5]	赵杰，李永明. 广义可能性计算树逻辑的两种范式[J]. 计算机科学与探索, 2016, 10(10): 1475-1481.
[6]	余鹏，魏欧，韩兰胜，牛耘. 模型检测网络传播干预策略[J]. 计算机科学与探索, 2014, 8(8): 906-918.
[7]	陈力琼1+ ,陈贤2 . 认证测试方法的改进及应用[J]. 计算机科学与探索, 2008, 2(1): 104-109.

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

Formal Method for Verifying BPEL Model Used by Functional Programming Language

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 7

编辑推荐

Metrics