Realizability Of Choreographies Using Petri Net

Service-oriented computing has emerged as a new software development paradigm that enables implementation of Webaccessible software systems that are composed of distributed services which interact with each other via exchanging messages.Such services are called Peer.In order to effectively integrate the independent Peer from different organizations and build the expected distributed system,it is necessary to provide the global contract that the Peers should abide by when Peer in the collaboration to produce message interaction.This contract that describes the message interaction between a group of Peers from the global perspective is called Choreography.The significance of the realizability analysis of Choreography is:In the case of a given choreography,the choreography is mapped to Peers,and then the Peers are combined under different communication conditions,and the message interaction between the Peers described by the Choreography implementation after combination conforms to the original Choreography.This article focuses on the realizability analysis of Choreography.This paper proposes a new method for the realizability analysis of Choreography based on interactive Petri net for the first time,specifically:(1)Expand the prototype Petri net into interactive Petri net and interactive interface Petri net to describe Choreography and Peers,and propose a method to map Choreography to Peers.This method firstly based on the interactive Petri net is defined,and then according to whether the Peers involved in the action Choreography of all actions can be divided into the action has nothing to do with action,and will not action mapping for tau(note:independent action),in the mapping process,the Peers keep relevant action,based on the connection between the flow at the same time,remove the tau.After removing the irrelevant action tau,the Peers obtained are equivalent to the Peers described in the original Choreography.(2)A method is proposed to analyze the realizability of Choreography under Synchronous Communication using Petri net.Under the Synchronous Communication model,this method fuses the message sending and message receiving actions that belong to different Peers,combines the Peers concurrently,and achieves the Choreographed Synchronization.Then the equivalence test protocol between the implementation of Choreographer Synchronization and Choreographer Synchronization is used to test whether the reachable graph of Choreographer and the reachable graph of original Choreographer satisfy the strong mutual simulation relationship.(3)A method is proposed to analyze the realizability of Choreography under bounded Asynchronous Communication using Petri net.Under the Asynchronous Communication model,this method realizes the Asynchronous Communication between Peers by adding buffer to the message receiving action,and gets the Asynchronous implementation of Choreography.Then the equivalence test protocol between the Asynchronous implementation of Choreography and Choreography is reduced to the test of whether the reachable graph of choreography and the reachable graph of original Choreography meet the weak mutual simulation relation.