Formal Verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows  

作　　者：曹军威 张帆 许可 刘连臣 吴澄 

机构地区：[1]CCF [2]ACM [3]IEEE [4]Research Institute of Information Technology,Tsinghua University [5]Tsinghua National Laboratory for Information Science and Technology [6]National CIMS Engineering and Research Center,Tsinghua University [7]Morgan Stanley

出　　处：《Journal of Computer Science & Technology》2011年第6期1017-1030,共14页计算机科学技术学报（英文版）

基　　金：supported by the National Basic Research 973 Program of China under Grant Nos.2011CB302805,2011CB302505;the National High Technology Research and Development 863 Program of China under Grant No.2011AA040501;the National Natural Science Foundation of China under Grant No.60803017;Fan 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.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.

关 键 词：grid computing workflow management formal verification state Pi calculus 

分 类 号：TP393.09[自动化与计算机技术—计算机应用技术]