Ensuring the correctness and reliability of large-scale resource sharing and complex job processing is an important task for
grid applications. From a formal method perspective, a grid service chain model based on state Pi calculus is proposed in
this work as the theoretical foundation for the service composition and collaboration in grid. Following the idea of the Web
Service Resource Framework (WSRF), state Pi calculus enables the life-cycle management of system states by associating the
actions in the original Pi calculus with system states. Moreover, model checking technique is exploited for the design-time
and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material
deformation structure is also provided to show the effectiveness of the proposed work.
Keywords grid - grid service chain - formal method - model checking - state Pi calculus
This article was recommended by Prof. Francis C.M. LAU, member of editorial board of Science in China.
Supported by the National Natural Science Foundation of China (Grant Nos. 60604033 and 60553001)