From Enabling to Ensuring Grid Workflows
Junwei Cao (Tsinghua University and Tsinghua National Laboratory for Information Science and Technology, China), Fan Zhang (Tsinghua University, China), Ke Xu (Tsinghua University, China) and Lianchen Liu (Tsinghua University, China)
Copyright: © 2009
Grid workflows are becoming a mainstream paradigm for implementing complex grid applications. In addition to existing grid enabling techniques, various grid ensuring techniques are emerging, e.g. workflow analysis and temporal reasoning, to probe potential pitfalls and errors and guarantee quality of services (QoS) at a design phase. A new state p calculus is proposed in this work, which not only enables flexible abstraction and management of historical grid system events, but also facilitates modeling and verification of grid workflows. Some typical patterns in grid workflows are captured and both static and dynamic formal verification issues are investigated, including structural correctness, specification satisfiability, logic satisfiability and consistency. A grid workflow modeling and verification environment, GridPiAnalyzer, is implemented using formal modeling and verification methods proposed in this work. Performance evaluation results are included using a grid workflow for gravitational wave data analysis.