Describing and Reasoning on the Composition of Grid Services Using Pi-Calculus

Composition of grid services combines two or more grid services to achieve the desired computing goals, which is becoming important in application from electronic commerce to application interoperation. Numerous frameworks have been proposed for the grid service composition; however, the fundamental research about the essential semantic specification of grid service composition has not been addressed. The imbalance development between the theory and the industry will directly affect QoS. Therefore, the research work on how to formalize and verify the behavior of composite grid services is imperative. Formal approaches offer an effective and unambiguous way to model, represent and verify the grid service composition. Under this premise, we attempt to use the pi-calculus to depict the dynamic, concurrent and interactive characteristic of grid service composition. A novel grid service composition signature has been proposed in this paper. Furthermore, based on the expansion to the pi-calculus, we presented the algebraic foundation of the model and formally semantic specification for the dynamic binding and interactive concurrency of the grid service composition.