›› 2011, Vol. 26 ›› Issue (6): 1017-1030.doi: 10.1007/s11390-011-1198-4

Special Issue: Theory and Algorithms

• Formal Methods • Previous Articles     Next Articles

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

Jun-Wei Cao1,2 (曹军威), Member, CCF, ACM, Senior Member, IEEE, Fan Zhang3 (张帆), Student Member, IEEE, Ke Xu4 (许可), Lian-Chen Liu3 (刘连臣) and Cheng Wu3 (吴澄)   

  1. 1. Research Institute of Information Technology, Tsinghua University, Beijing 100084, China;
    2. Tsinghua National Laboratory for Information Science and Technology, Beijing 100084, China;
    3. National CIMS Engineering and Research Center, Tsinghua University, Beijing 100084, China;
    4. Morgan Stanley, Shanghai 200002, China
  • Received:2010-10-29 Revised:2011-09-13 Online:2011-11-05 Published:2011-11-05
  • About author:Jun-Wei Cao received his Ph.D. degree in computer science from the University of Warwick, Coventry, UK, in 2001. He received his B.S. and M.S. degrees in control theories and engineering in 1996 and 1998, re-spectively, both from Tsinghua Uni-versity, Beijing, China. He is cur-rently a professor and vice direc-tor, Research Institute of Informa-tion Technology, Tsinghua University. He is also with Ts-inghua National Laboratory for Information Science and Technology. He is now a visiting scientist of MIT. Before joining Tsinghua University in 2006, he was a research sci-entist at MIT LIGO Laboratory and NEC Laboratories Eu-rope for about 5 years. He has published over 120 papers, which have been cited by international scholars for over 2200 times. He has authored or edited 5 books and proceedings. His research is focused on advanced computing technologies and applications. Prof. Cao is a Senior Member of the IEEE Computer Society and a Member of the ACM and CCF.
    Fan Zhang received the B.S. de-gree in computer science from Hubei Univ. Technology and M.S. degree in control science and engineering from Huazhong University of Science and Technology. He is currently a Ph.D. student in the Department of Au-tomation, Tsinghua University. His research interests include data center networks and grid/cloud computing
  • Supported by:

    This work is 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, and 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 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

[1] Foster I, Kesselman C. The Grid: Blueprint for a New ComputingInfrastructure. San Fransisco: Morgan-Kaufmann,1998.

[2] Cao J, Jarvis S A, Saini S, Nudd G R. GridFlow: Workflowmanagement for grid computing. In Proc. the 3rdIEEE/ACM Int. Symp. on Cluster Computing and the Grid,Tokyo, Japan, May 12-15, 2003, pp.198-205.

[3] Brown D A, Brady P R et al. A case study on the use of workflowtechnologies for scientific analysis: Gravitational wavedata analysis. In Workflows for eScience: Scientific Work-flows for Grids, Taylor I J, Dealman E, Gannon D B et al(eds.), Springer Verlag, 2007, pp.39-59.

[4] Cao J, Fingberg J, Berti G et al. Implementation of gridenabledmedical simulation applications using workflow techniques.In Proc. the 2nd Int. Workshop on Grid and Cooper-ative Computing, Shanghai, China, Dec. 7-10, 2003, pp.34-41.

[5] Liu Y, M¨uller S, Xu K. A static compliance checking frameworkfor business process models. IBM Systems Journal,2007, 46(2): 335-362.

[6] Chen J, Yang Y. A taxonomy of grid workflow verification andvalidation. Concurrency and Computation: Practice and Ex-perience, 2008, 20(4): 347-360.

[7] Chen J, Yang Y. Multiple states based temporal consistencyfor dynamic verification of fixed-time constraints in grid workflowsystems. Concurrency and Computation: Practice andExperience, 2007, 19(7): 965-982.

[8] Tan W, Fan Y, Zhou M. A petri net-based method for compatibilityanalysis and composition ofWeb services in businessprocess execution Language. IEEE Transactions on Automa-tion Science and Engineering, 2009, 6(1): 94-106.

[9] Tan W, Fan Y, Zhou M et al. Data-driven service compositionin enterprise SOA solutions: A petri net approach.IEEE Trans. Automation Science and Engineering, 2010,7(3): 686-694.

[10] Li X, Fan Y, Sheng Q Z et al. A petri net approach to analyzingbehavioral compatibility and similarity of Web services.IEEE Trans. Systems, Man, and Cybernetics, Part A: Sys-tems and Humans, 2010, 41(3): 510-521.

[11] Xiong P, Fan Y, Zhou M. Web service configuration undermultiple quality-of-service attribute. IEEE Trans. Automa-tion Science and Engineering, 2009, 6(2): 311-321.

[12] Xiong P, Fan Y, Zhou M. QoS-aware Web service configuration.IEEE Trans. Systems, Man and Cybernetics, Part A,2008, 38(4): 888-895.

[13] Clarke E M, Grumberg O, Peled D A. Model Checking, MITPress, 1999.

[14] Xu K,Wang Y X,Wu C. Formal verification technique for gridservice chain model and its application. Science in China, Se-ries F: Information Sciences, 2007, 50(1): 1-20.

[15] Xu K, Cao J, Liu L, Wu C. Performance optimization of temporalreasoning for grid workflows using relaxed region analysis.In Proc. the 22nd IEEE Int. Conf. Advanced Infor-mation Networking and Applications Workshops, GinoWan,Japan, March 25-28, 2008, pp.187-194.

[16] Salaün G, Bordeaux L, Schaerf M. Describing and reasoningon Web services using process algebra. In Proc. Int. Conf.Web Services, San Diego, USA, June 6-9, 2004, pp.43-50.

[17] Németh Z, Sunderam V. Characterizing grids: Attributes,definitions, and formalisms. J. Grid Computing, 2003, 1(1):9-23.

[18] Huang S, Mulcahy J J. Software reuse in the evolution of ane-commerce system: A case study. International Journal ofComputing & Information Technology, 2(1): 1-15.

[19] Cai H. Scale-free Web services. In Proc. Int. Conf. WebServices, Salt Lake City, USA, July 9-13, 2007, pp.288-295.

[20] Milner R. Communicating and Mobile Systems: the Pi Calculus.Cambridge University Press, 1999.

[21] Wang S, Armstrong M P. A quadtree approach to domaindecomposition for spatial interpolation in grid computing environments.Parallel Computing, 2003, 29(10): 1481-1504.

[22] Cimatti A, Clarke E et al. NuSMV2: An open source tool forsymbolic model checking. In Proc. the 14th Int. Conf. Com-puter Aided Verification, Copenhagen, Denmark, July 27-31,2002, 359-364.

[23] Deelman E, Kesselman C et al. GriPhyN and LIGO, buildinga virtual data grid for gravitational wave scientists. In Proc.the 11th Int. Symp. High Performance Distributed Comput-ing, Edinburgh, Scotland, July 24-26, 2002, pp.225-234.

[24] Liu R, Kumar A. An analysis and taxonomy of unstructuredworkflows. In Proc. the 3rd Int. Conf. Business ProcessManagement, Nancy, France, Sept. 5-9, 2005, pp.268-284.

[25] Grumberg O, Long D E. Model checking and modular verification.ACM Transactions on Programming Languages andSystems, 1999, 16(3): 843-871.
No related articles found!
Full text



[1] Liu Mingye; Hong Enyu;. Some Covering Problems and Their Solutions in Automatic Logic Synthesis Systems[J]. , 1986, 1(2): 83 -92 .
[2] Chen Shihua;. On the Structure of (Weak) Inverses of an (Weakly) Invertible Finite Automaton[J]. , 1986, 1(3): 92 -100 .
[3] Gao Qingshi; Zhang Xiang; Yang Shufan; Chen Shuqing;. Vector Computer 757[J]. , 1986, 1(3): 1 -14 .
[4] Chen Zhaoxiong; Gao Qingshi;. A Substitution Based Model for the Implementation of PROLOG——The Design and Implementation of LPROLOG[J]. , 1986, 1(4): 17 -26 .
[5] Huang Heyan;. A Parallel Implementation Model of HPARLOG[J]. , 1986, 1(4): 27 -38 .
[6] Min Yinghua; Han Zhide;. A Built-in Test Pattern Generator[J]. , 1986, 1(4): 62 -74 .
[7] Tang Tonggao; Zhao Zhaokeng;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[8] Min Yinghua;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[9] Zhu Hong;. Some Mathematical Properties of the Functional Programming Language FP[J]. , 1987, 2(3): 202 -216 .
[10] Li Minghui;. CAD System of Microprogrammed Digital Systems[J]. , 1987, 2(3): 226 -235 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved