With quick development of grid techniques and growing complexity of grid applications, it is becoming critical for reasoning temporal properties of grid workflows to probe potential pitfalls and errors, in order to en...With quick development of grid techniques and growing complexity of grid applications, it is becoming critical for reasoning temporal properties of grid workflows to probe potential pitfalls and errors, in order to ensure reliability and trustworthiness at the initial design phase. A state Pi calculus is proposed and implemented in this work, which not only enables fexible abstraction and management of historical grid verification of grid workflows. Furthermore, a relaxed region system events, but also facilitates modeling and temporal analysis （RRA） approach is proposed to decompose large scale grid workflows into sequentially composed regions with relaxation of parallel workflow branches, and corresponding verification strategies are also decomposed following modular verification principles. Performance evaluation results show that the RRA approach can dramatically reduce CPU time and memory usage of formal verification.展开更多
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 sta...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 exploltad 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.展开更多
基金supported by the National Basic Research 973 Program of China under Grant Nos.2011CB302805,2011CB302505the National High Technology Research and Development 863 Program of China under Grant No.2011AA040501+1 种基金the National Natural Science Foundation of China under Grant No.60803017Fan Zhang is supported by IBM 2011-2012 Ph.D. Fellowship
文摘With quick development of grid techniques and growing complexity of grid applications, it is becoming critical for reasoning temporal properties of grid workflows to probe potential pitfalls and errors, in order to ensure reliability and trustworthiness at the initial design phase. A state Pi calculus is proposed and implemented in this work, which not only enables fexible abstraction and management of historical grid verification of grid workflows. Furthermore, a relaxed region system events, but also facilitates modeling and temporal analysis （RRA） approach is proposed to decompose large scale grid workflows into sequentially composed regions with relaxation of parallel workflow branches, and corresponding verification strategies are also decomposed following modular verification principles. Performance evaluation results show that the RRA approach can dramatically reduce CPU time and memory usage of formal verification.
基金Supported by the National Natural Science Foundation of China (Grant Nos. 60604033 and 60553001)
文摘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 exploltad 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.
