摘要:将编排映射为Peer（参与者），是对编排进行可实现性分析的第1个步骤.现有文献提出的映射方法未考虑参与者中τ对行为的影响，无法确保编排与参与者间的行为一致性.以Petri网作为形式化基础，提出了一种能够保持编排与参与者间行为一致的映射方法，允许：（1）通过动作映射，将交互式Petri网定义的编排映射为带τ的交互式Petri网；（2）提出了4条τ删除规则，用以对带τ的交互式Petri网中的τ进行有选择的删除；（3）将编排与参与者间的行为一致性问题规约为检验两个交互式Petri间是否满足弱互模拟的问题，并证明了这4条τ删除规则的正确性.实验结果表明，该映射方法能够确保编排与参与者间的行为一致性.



Abstract: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 τ.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 τ through action projection from a choreography defined by an interaction Petri net,2) develop four types of tau deletion rules to selectively delete τ 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.



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/5382