基于Petri网自动化构建BPEL流程的SMV模型  

SMV Model for Automating the Construction of BPEL Process Based on Petri Net

作　　者：周子健 刘冬梅[1] ZHOU Zijian;LIU Dongmei(School of Computer Science,Nanjing University of Science and Technology,Nanjing 210094)

机构地区：[1]南京理工大学计算机学院,南京210094

出　　处：《计算机与数字工程》2021年第10期2062-2068,2132,共8页Computer & Digital Engineering

摘　　要：针对使用BPEL进行Web服务组合过程中,复杂业务流程的正确性验证繁琐且易出错问题,论文提出了一种自动化构建BPEL流程的SMV模型方法。该方法将BPEL流程自动化映射到Petri网,借由Petri网直观展示组合流程并进行边界值、死锁等性质的检查,再由Petri网可达图自动化生成SMV模型,使用模型检测工具验证系统的安全性和行为属性,从而在流程的设计阶段发现服务组合中可能存在的问题。实验结果表明论文工作可以有效地减少验证过程的复杂性,有助于提高服务组合流程的正确性。Aiming at the tedious and error-prone problem of verifying the correctness of complex business processes in the process of web service composition using BPEL,this paper proposes an SMV model method for automatically constructing BPEL processes.This method automatically maps the BPEL process to the Petri net,and uses the Petri net to visually display the combined process and check the boundary value,deadlock and other properties.This method uses the Petri net reachability graph to automatically generate SMV models,and uses model checking tools to verify the security and behavioral attributes of the system,so as to find possible problems in the service composition during the design phase of the process.The experimental results show that this work can effectively reduce the complexity of the verification process and help improve the correctness of the service composition process.

关 键 词：服务组合 BPEL PETRI网 模型检测 

分 类 号：TP393.11[自动化与计算机技术—计算机应用技术]