Journal of Frontiers of Computer Science and Technology ›› 2018, Vol. 12 ›› Issue (2): 185-196.DOI: 10.3778/j.issn.1673-9418.1611056

Previous Articles     Next Articles

Formal Method for Verifying BPEL Model Used by Functional Programming Language

ZHU Yi1,2+, HUANG Zhiqiu1, ZHOU Hang1   

  1. 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

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

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

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

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

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

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