A sound and complete theory of graph transformations for service programming with sessions and pipelines

Graph transformation techniques, the Double-Pushout (DPO) approach in particular, have been successfully applied in the modeling of concurrent systems. In this area, a research thread has addressed the definition of concurrent semantics for process calculi. In this paper, we propose a theory of graph transformations for service programming with sophisticated features such as sessions and pipelines. Through graph representation of CaSPiS, a recently proposed process calculus, we show how graph transformations can cope with advanced features of service-oriented computing, such as several logical notions of scoping together with the interplay between linking and containment. We first exploit a graph algebra and set up a graph model that supports graph transformations in the DPO approach. Then, we show how to represent CaSPiS processes as hierarchical graphs in the graph model and their behaviors as graph transformation rules. Finally, we provide the soundness and completeness results of these rules with respect to the reduction semantics of CaSPiS.