Title
Formal Verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows
Abstract
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 flexible abstraction and management of historical grid system events, but also facilitates modeling and temporal verification of grid workflows. Furthermore, a relaxed region 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
Year
DOI
Venue
2011
10.1007/s11390-011-1198-4
J. Comput. Sci. Technol.
Keywords
Field
DocType
state Pi calculus,grid computing,workflow management,formal verification
Computer science,Workflow,Grid,Formal verification,Distributed computing
Journal
Volume
Issue
ISSN
26
6
1860-4749
Citations 
PageRank 
References 
1
0.36
16
Authors
10
Name
Order
Citations
PageRank
Junwei Cao193570.95
Junwei Cao293570.95
Fan Zhang3998.65
Ke Xu410.36
Lianchen Liu5619.11
Cheng Wu6115493.20
张帆740.72
许可810.69
刘连臣910.36
吴澄1010.69