一种保持编排与参与者间行为一致的映射方法  

Projection Approach for Keeping the Behavior Consistency Between Choreography and Peers

作　　者：代飞 陈凤强[3] 莫启[2,3] 王炜[2,3] 李彤[2,3] 梁志宏[1,2] DAI Fei1,2, CHEN Feng-Qiang3, MO Qi2,3, WANG Wei2,3, LI Tong2,3, LIANG Zhi-Hong1,2(1.School of Big Data and Intelligence Engineering, Yunnan University, Kunming 650224, China; 2.Key Laboratory for Software Engineering of Yunnan Province （Yunnan University）, Kunming 650091, China; 3.School of Software, Yunnan University, Kunming 650091, China)

机构地区：[1]西南林业大学大数据与智能工程学院,云南昆明650224 [2]云南省软件工程重点实验室(云南大学),云南昆明650091 [3]云南大学软件学院,云南昆明650091

出　　处：《软件学报》2018年第5期1451-1470,共20页Journal of Software

基　　金：国家自然科学基金(61462095;61702442;61462092;61379032);云南省自然科学基金(2016FB102);云南省教育厅科学研究基金重大专项(ZD2014001)~~

摘　　要：将编排映射为Peer(参与者),是对编排进行可实现性分析的第1个步骤.现有文献提出的映射方法未考虑参与者中τ对行为的影响,无法确保编排与参与者间的行为一致性.以Petri网作为形式化基础,提出了一种能够保持编排与参与者间行为一致的映射方法,允许:(1)通过动作映射,将交互式Petri网定义的编排映射为带τ的交互式Petri网;(2)提出了4条τ删除规则,用以对带τ的交互式Petri网中的τ进行有选择的删除;(3)将编排与参与者间的行为一致性问题规约为检验两个交互式Petri间是否满足弱互模拟的问题,并证明了这4条τ删除规则的正确性.实验结果表明,该映射方法能够确保编排与参与者间的行为一致性.That peers are generated by projection from choreographies is known as the first step in checking choreographies＇ realizability. However, the projection approaches proposed by the existing literature have not considered the behavioral influence of invisible action r. This leads to behavior inconsistency between choreography and the generated peers. This paper proposes a projection approach based on Petri nets. which allows us to 1） generate the peers defined by interaction Petri nets with r through action projection from a choreography defined by an interaction Petri net, 2） develop four types of tau deletion rules to selectively delete r of interaction Petri nets, and 3） specify the behavior consistency between choreography and the generated peers to check whether two Petri nets meet the weak simulation. Moreover, the correctness of these four types of tau deletion rules is proved. Experimental results show that the projection approach can ensure the behavior consistency between choreography and peers.

关 键 词：业务过程管理 编排 参与者 映射 可实现性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]