Research On The Theory And Application Of The State π Calculus Based Formal Verification For Grid Service Flows

Grid service flow is an important paradigm for realizing complex heterogeneous resource collaboration and sharing in various grid applications. Correctness verification in the design and implementation of grid service flows is an active research topic in the domain of system science and computer science which enjoys both great theoretical and practical values. Based on realistic applications like LIGO data grid, this dissertation has systematically investigated the formal modeling, verification and its performance issues for grid service flows by proposing a calculus called the stateπcalculus and the study of its formal verification support.Following the new feature of stateful resource management introduced in the Web Service Resource Framework, first a new stateπcalculus is proposed to further strengthen its capability in managing the life-cycle of system states. The proposed calculus not only enables the flexible abstraction and management of historical system events, but also facilitates the modeling and verification of grid service flows. Moreover, based on the stateπcalculus, the formal semantics of grid service execution and selection, the specification of BPEL4WS, DAGMan and the parallel / pipeline patterns in grid service flows are also rigidly captured, which at the same time has verified the full expressiveness of our stateπcalculus.Based on the formal semantics of grid service flows with stateπcalculus, the dissertation fully studies from both the static and dynamic aspects of its formal verification issues including its structural correctness, specification satisfiability, business logic satisfiability and consistency. Systematic solution is provided for the above issues by the proposal of strong/weak state assertion for our stateπcalculus with its model checking support. By the gravitational wave data analysis application from LIGO data grid, it is shown the proposed solution enjoys the advantages of: (1) supports the state / event hybrid analysis and model checking of stateπcalculus models; (2) reduce unnecessary verifications to save the verification cost; (3) be independent of specific model checking engine and thus enjoys a wider choice of new formal verification techniques.Furthermore, the improvement of verification performance is also investigated by following the two ideas of grid service flow decomposition and process bug patterns respectively. On the one hand, by decomposing a grid service flow into a set of sequential standard regions with parallel branches, the corresponding verification strategy is also decomposed following the idea of modular verification. On the other hand, by identifying the potential process bug patterns in the structure of grid service flows, the idea of guided search is combined into the formal verification of grid service flow to efficiently falsify its correctness. With the performance evaluation on verifying multiple gravitational wave data analysis applications with different complexity from LIGO, it is illustrated that the proposed approaches can effectively reduce both the required CPU time and memory cost compared to using various traditional verification approaches alone.Finally, the framework and application background of GridPiAnalyzer, an automatic tool support for the formal verification of grid service flows based on this dissertation, is introduced. It currently provides the support for Condor DAGMan, BPEL4WS 1.1 specification and IBM's Websphere Business Integrator TM model.