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

Analyzing realizability of choreographies using Petri nets

作　　者：黄苾 代飞 王亚博 莫启[2] 曹涌 王雷光 HUANG Bi;DAI Fei;WANG Yabo;MO Qi;CAO Yong;WANG Leiguang(School of Big Data and Intelligence Engineering,Southwest Forestry University,Kunming 650224,China;School of Software,Yunnan University,Kunming 650091,China)

机构地区：[1]西南林业大学大数据与智能工程学院,云南昆明650224 [2]云南大学软件学院,云南昆明650091

出　　处：《计算机集成制造系统》2020年第6期1548-1556,共9页Computer Integrated Manufacturing Systems

基　　金：国家自然科学基金资助项目(61702442,61862065);云南省应用基础研究资助项目(2018FB105)。

摘　　要：为了解决编排建模中存在的可实现性问题,即给定一个编排,检测编排生成的参与者间的交互与编排规约是否完全匹配,从同步通信和异步通信两个方面,提出了一种使用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.

关 键 词：编排 可实现性 异步通信 同步通信 PETRI网 

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