A modelling approach to formally represent service orchestration

摘要

This paper presents a methodology to formally model service orchestration. The methodology is based on a set of selected flow descriptors, which are expressed in a Petri net derived formalism. The chosen descriptors cover concurrency, synchronisation, multithreading, looping and conditional execution. The modelling of temporal and logical conditions arising in conjunction with looping constructs is dedicated a satellite set of models. The formal definition of the translation procedure for the structured activities of the main set is given. The means of calculating the relationship between the timing constraints of the constructs used to specify the orchestration and the intermediate constraints of the composing services are studied. The paper concludes with a presentation of the industrial demonstrator used in this research and a discussion about the advantages and disadvantages of the presented modelling approach, at verification stage.