Redouane Nouara and Allaoua Chaoui, University Abdel Hamid Mehri Constantine 2, Algeria

The success of Service Oriented Architecture (SOA) largely depended on the success of automatic service composition. Dynamic service selection process should ensure full compatibility between the services involved in the composition. This compatibility must be both on static proprieties, called interface compatibility which can be easily proved and especially on behavioural compatibility that needs composability checking of basic services. In this paper, we propose (1) a formalism for modelling composite services using an extension of the Business Process (BP) modelling approach proposed by Benatallah et al. and (2) a formal verification approach of service composition. This approach uses the Graph Transformation (GT) methodology as a formal verification tool. It allows behavioural compatibility verification of two given services modelled by their BPs, used as the source graph in the GT operation. The idea consists of (1) trying to dynamically generate a graph grammar R (a set of transformation rules) whose application generates the composite service, if it exists, in this case (2) the next step consist in checking the deadlock free in the resulting composite service. To this end we propose an algorithm that we have implemented using the AGG, an algebraic graph transformation API environment under eclipse IDE.

Dynamic Service Composition, Graph Transformation, Service Composition Checking, Modeling Composite Service