A mechanism for grid service composition behavior specification and verification

Current grid service choreography proposals remain at the descriptive level, without providing any kind of reasoning mechanism to check the compatibility and validity of grid service composition. How to formalize and verify the behavior of the grid service composition is therefore imperative. A novel process algebra, Cpi-calculus (Conditional Pi-calculus), is proposed in this paper. By analyzing the interactive behavior of composite grid services, we present a grid service composition signature. Based on the signature, we construct Interactive Behavior Model (IABM) for grid service composition and specify the interactive behavior using the Cpi-calculus. The case study shows that the mechanism for grid service specification and verification could be the algebraic foundation to be used afterwards in automatic and dynamic composition.