{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T03:43:41Z","timestamp":1761968621050,"version":"build-2065373602"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2011,11,1]],"date-time":"2011-11-01T00:00:00Z","timestamp":1320105600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2011,11]]},"DOI":"10.1007\/s11390-011-1198-4","type":"journal-article","created":{"date-parts":[[2011,11,28]],"date-time":"2011-11-28T13:47:57Z","timestamp":1322488077000},"page":"1017-1030","source":"Crossref","is-referenced-by-count":5,"title":["Formal Verification of Temporal Properties for Reduced Overhead in Grid Scientific Workflows"],"prefix":"10.1007","volume":"26","author":[{"given":"Jun-Wei","family":"Cao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ke","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lian-Chen","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cheng","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,11,28]]},"reference":[{"key":"1198_CR1","volume-title":"The Grid: Blueprint for a New Computing Infrastructure","author":"I Foster","year":"1998","unstructured":"Foster I, Kesselman C. The Grid: Blueprint for a New Computing Infrastructure. San Fransisco: Morgan-Kaufmann, 1998."},{"key":"1198_CR2","doi-asserted-by":"crossref","unstructured":"Cao J, Jarvis S A, Saini S, Nudd G R. GridFlow: Workflow management for grid computing. In Proc. the 3rd IEEE\/ACM Int. Symp. on Cluster Computing and the Grid, Tokyo, Japan, May 12\u201315, 2003, pp.198-205.","DOI":"10.1109\/CCGRID.2003.1199369"},{"key":"1198_CR3","unstructured":"Brown D A, Brady P R et al. A case study on the use of workflow technologies for scientific analysis: Gravitational wave data analysis. In Workflows for eScience: Scientific Workflows for Grids, Taylor I J, Dealman E, Gannon D B et al (eds.), Springer Verlag, 2007, pp.39-59."},{"key":"1198_CR4","doi-asserted-by":"crossref","unstructured":"Cao J, Fingberg J, Berti G et al. Implementation of grid-enabled medical simulation applications using workflow techniques. In Proc. the 2nd Int. Workshop on Grid and Cooperative Computing, Shanghai, China, Dec. 7\u201310, 2003, pp.34-41.","DOI":"10.1007\/978-3-540-24679-4_14"},{"issue":"2","key":"1198_CR5","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1147\/sj.462.0335","volume":"46","author":"Y Liu","year":"2007","unstructured":"Liu Y, M\u00fcller S, Xu K. A static compliance checking framework for business process models. IBM Systems Journal, 2007, 46(2): 335\u2013362.","journal-title":"IBM Systems Journal"},{"issue":"4","key":"1198_CR6","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1002\/cpe.1220","volume":"20","author":"J Chen","year":"2008","unstructured":"Chen J, Yang Y. A taxonomy of grid workflow verification and validation. Concurrency and Computation: Practice and Experience, 2008, 20(4): 347\u2013360.","journal-title":"Concurrency and Computation: Practice and Experience"},{"issue":"7","key":"1198_CR7","doi-asserted-by":"crossref","first-page":"965","DOI":"10.1002\/cpe.1088","volume":"19","author":"J Chen","year":"2007","unstructured":"Chen J, Yang Y. Multiple states based temporal consistency for dynamic verification of fixed-time constraints in grid workflow systems. Concurrency and Computation: Practice and Experience, 2007, 19(7): 965\u2013982.","journal-title":"Concurrency and Computation: Practice and Experience"},{"issue":"1","key":"1198_CR8","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1109\/TASE.2008.916747","volume":"6","author":"W Tan","year":"2009","unstructured":"Tan W, Fan Y, Zhou M. A petri net-based method for compatibility analysis and composition ofWeb services in business process execution Language. IEEE Transactions on Automation Science and Engineering, 2009, 6(1): 94\u2013106.","journal-title":"IEEE Transactions on Automation Science and Engineering"},{"issue":"3","key":"1198_CR9","doi-asserted-by":"crossref","first-page":"686","DOI":"10.1109\/TASE.2009.2034016","volume":"7","author":"W Tan","year":"2010","unstructured":"Tan W, Fan Y, Zhou M et al. Data-driven service composition in enterprise SOA solutions: A petri net approach. IEEE Trans. Automation Science and Engineering, 2010, 7(3): 686\u2013694.","journal-title":"IEEE Trans. Automation Science and Engineering"},{"key":"1198_CR10","doi-asserted-by":"crossref","unstructured":"Li X, Fan Y, Sheng Q Z et al. A petri net approach to analyzing behavioral compatibility and similarity of Web services. IEEE Trans. Systems, Man, and Cybernetics, Part A: Systems and Humans, 2010, 41(3): 510\u2013521.","DOI":"10.1109\/TSMCA.2010.2093884"},{"issue":"2","key":"1198_CR11","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1109\/TASE.2008.2009103","volume":"6","author":"P Xiong","year":"2009","unstructured":"Xiong P, Fan Y, Zhou M. Web service configuration under multiple quality-of-service attribute. IEEE Trans. Automation Science and Engineering, 2009, 6(2): 311\u2013321.","journal-title":"IEEE Trans. Automation Science and Engineering"},{"issue":"4","key":"1198_CR12","doi-asserted-by":"crossref","first-page":"888","DOI":"10.1109\/TSMCA.2008.923062","volume":"38","author":"P Xiong","year":"2008","unstructured":"Xiong P, Fan Y, Zhou M. QoS-aware Web service configuration. IEEE Trans. Systems, Man and Cybernetics, Part A, 2008, 38(4): 888\u2013895.","journal-title":"IEEE Trans. Systems, Man and Cybernetics, Part A"},{"key":"1198_CR13","unstructured":"Clarke E M, Grumberg O, Peled D A. Model Checking, MIT Press, 1999."},{"issue":"1","key":"1198_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s11432-007-0006-9","volume":"50","author":"K Xu","year":"2007","unstructured":"Xu K,Wang Y X,Wu C. Formal verification technique for grid service chain model and its application. Science in China, Series F: Information Sciences, 2007, 50(1): 1\u201320.","journal-title":"Science in China, Series F: Information Sciences"},{"key":"1198_CR15","doi-asserted-by":"crossref","unstructured":"Xu K, Cao J, Liu L, Wu C. Performance optimization of temporal reasoning for grid workflows using relaxed region analysis. In Proc. the 22nd IEEE Int. Conf. Advanced Information Networking and Applications Workshops, GinoWan, Japan, March 25\u201328, 2008, pp.187-194.","DOI":"10.1109\/WAINA.2008.48"},{"key":"1198_CR16","doi-asserted-by":"crossref","unstructured":"Sala\u00fcn G, Bordeaux L, Schaerf M. Describing and reasoning on Web services using process algebra. In Proc. Int. Conf. Web Services, San Diego, USA, June 6\u20139, 2004, pp.43-50.","DOI":"10.1109\/ICWS.2004.1314722"},{"issue":"1","key":"1198_CR17","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1023\/A:1024011025052","volume":"1","author":"Z N\u00e9meth","year":"2003","unstructured":"N\u00e9meth Z, Sunderam V. Characterizing grids: Attributes, definitions, and formalisms. J. Grid Computing, 2003, 1(1): 9\u201323.","journal-title":"J. Grid Computing"},{"key":"1198_CR18","doi-asserted-by":"crossref","unstructured":"Huang S, Mulcahy J J. Software reuse in the evolution of an e-commerce system: A case study. International Journal of Computing & Information Technology, 2(1): 1\u201315.","DOI":"10.5958\/j.0975-8070.1.1.004"},{"key":"1198_CR19","doi-asserted-by":"crossref","unstructured":"Cai H. Scale-free Web services. In Proc. Int. Conf. Web Services, Salt Lake City, USA, July 9\u201313, 2007, pp.288-295.","DOI":"10.1109\/ICWS.2007.156"},{"key":"1198_CR20","unstructured":"Milner R. Communicating and Mobile Systems: the Pi Calculus. Cambridge University Press, 1999."},{"issue":"10","key":"1198_CR21","doi-asserted-by":"crossref","first-page":"1481","DOI":"10.1016\/j.parco.2003.04.003","volume":"29","author":"S Wang","year":"2003","unstructured":"Wang S, Armstrong M P. A quadtree approach to domain decomposition for spatial interpolation in grid computing environments. Parallel Computing, 2003, 29(10): 1481\u20131504.","journal-title":"Parallel Computing"},{"key":"1198_CR22","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke E et al. NuSMV2: An open source tool for symbolic model checking. In Proc. the 14th Int. Conf. Computer Aided Verification, Copenhagen, Denmark, July 27\u201331, 2002, 359\u2013364.","DOI":"10.1007\/3-540-45657-0_29"},{"key":"1198_CR23","doi-asserted-by":"crossref","unstructured":"Deelman E, Kesselman C et al. GriPhyN and LIGO, building a virtual data grid for gravitational wave scientists. In Proc. the 11th Int. Symp. High Performance Distributed Computing, Edinburgh, Scotland, July 24\u201326, 2002, pp.225-234.","DOI":"10.1109\/HPDC.2002.1029922"},{"key":"1198_CR24","doi-asserted-by":"crossref","unstructured":"Liu R, Kumar A. An analysis and taxonomy of unstructured workflows. In Proc. the 3rd Int. Conf. Business Process Management, Nancy, France, Sept. 5\u20139, 2005, pp.268-284.","DOI":"10.1007\/11538394_18"},{"issue":"3","key":"1198_CR25","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1999","unstructured":"Grumberg O, Long D E. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 1999, 16(3): 843\u2013871.","journal-title":"ACM Transactions on Programming Languages and Systems"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-011-1198-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-011-1198-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-011-1198-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,14]],"date-time":"2025-03-14T15:51:45Z","timestamp":1741967505000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-011-1198-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11]]},"references-count":25,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,11]]}},"alternative-id":["1198"],"URL":"https:\/\/doi.org\/10.1007\/s11390-011-1198-4","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"type":"print","value":"1000-9000"},{"type":"electronic","value":"1860-4749"}],"subject":[],"published":{"date-parts":[[2011,11]]}}}