基于Petri网分析编排的可实现性

Analyzing realizability of choreographies using Petri nets

为了解决编排建模中存在的可实现性问题,即给定一个编排,检测编排生成的参与者间的交互与编排规约是否完全匹配,从同步通信和异步通信两个方面,提出了一种使用Petri网分析编排可实现性的方法。首先,使用映射和约简操作,实现了从编排中自动生成参与者。然后,使用强互模拟关系,分析了同步通信下编排的可实现性。最后,使用弱互模拟关系,分析了有界异步通信下编排的可实现性。实验结果表明了所提方法的有效性。

Aiming at the problem of realizability during the process of modeling choreographies,an approach for analyzing realizability of choreographies using Petri nets was proposed from two aspects of synchronous communication and asynchronous communication.In this method,the peers from the given choreography was generated automatically,and the realizability of choreographies under synchronous communication was checked using strong bisimulation.The realizability of choreographies under bounded asynchronous communication was analyzed using weak bisimulation.The effectiveness of the proposed method was verified by experimental results.