{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T18:18:16Z","timestamp":1761675496989},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,2,1]],"date-time":"2007-02-01T00:00:00Z","timestamp":1170288000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SCI CHINA SER F"],"published-print":{"date-parts":[[2007,2]]},"DOI":"10.1007\/s11432-007-0006-9","type":"journal-article","created":{"date-parts":[[2007,6,27]],"date-time":"2007-06-27T16:41:05Z","timestamp":1182962465000},"page":"1-20","source":"Crossref","is-referenced-by-count":5,"title":["Formal verification technique for grid service chain model and its application"],"prefix":"10.1007","volume":"50","author":[{"given":"Ke","family":"Xu","sequence":"first","affiliation":[]},{"given":"YueXuan","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Cheng","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Joseph J, Fellenstein C. Grid Computing. IBM Press, 2003. 3\u201325"},{"key":"6_CR2","first-page":"107","volume-title":"Proc. 9th IEEE Int. Conf. on Engineering of Complex Computer Systems","author":"T. Bolognesi","year":"2004","unstructured":"Bolognesi T. A conceptual framework for state-based and event-based formal behavioral specification languages. In: Pierfrancesco B, Shawn A B, Bernhard S, eds. Proc. 9th IEEE Int. Conf. on Engineering of Complex Computer Systems. CA: IEEE Press, 2004. 107\u2013116"},{"key":"6_CR3","series-title":"Lect Notes in Comput Sci","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1007\/11745693_53","volume-title":"Advances in Grid and Pervasive Computing","author":"K. Xu","year":"2006","unstructured":"Xu K, Wang Y X, Wu C. Ensuring secure and robust grid applications \u2014 from a formal method point of view. In: Chung Y C, Moreira J E, eds. Advances in Grid and Pervasive Computing. Lect Notes in Comput Sci, Vol 3947. Beilin: Springer-Verlag, 2006. 537\u2013546"},{"key":"6_CR4","series-title":"Lect Notes in Comput Sci","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/11577188_6","volume-title":"Network and Parallel Computing","author":"Y. X. Wang","year":"2005","unstructured":"Wang Y X, Wu C, Xu K. Study on Pi-calculus based equipment grid service chain model. In: Jin H, Reed D A, Jiang W, eds. Network and Parallel Computing. Lect Notes in Comput Sci, Vol 3779. Beilin: Springer-Verlag, 2005. 40\u201347"},{"key":"6_CR5","first-page":"1","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge: MIT Press, 1999. 1\u201397"},{"issue":"1","key":"6_CR6","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 Comput, 2003, 1(1): 9\u201323","journal-title":"J Grid Comput"},{"issue":"3","key":"6_CR7","first-page":"417","volume":"15","author":"Z. N\u00e9meth","year":"2002","unstructured":"N\u00e9meth Z. Definition of a parallel execution model with abstract state machine. Acta Cybernet, 2002, 15(3): 417\u2013455","journal-title":"Acta Cybernet"},{"key":"6_CR8","first-page":"11","volume-title":"The Pi-calculus: a Theory of Mobile Processes","author":"D. Sangiorgi","year":"1999","unstructured":"Sangiorgi D, Walker D. The Pi-calculus: a Theory of Mobile Processes. Cambridge: Cambridge University Press, 1999. 11\u2013154"},{"key":"6_CR9","first-page":"97","volume-title":"Proc. Specification and Verification of Component-Based Systems","author":"C. Pahl","year":"2001","unstructured":"Pahl C. A Pi-calculus based framework for the composition and replacement of components. In: Giannakopoulou D, Leavens G T, Sitaraman M, eds. Proc. Specification and Verification of Component-Based Systems. USA: ACM Press, 2001. 97\u2013107"},{"key":"6_CR10","series-title":"Lect Notes in Comput Sci","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/11596370_43","volume-title":"Coordination Models and Languages","author":"M. Manuei","year":"2005","unstructured":"Manuei M, Sergio G. A case study of web services orchestration. In: Jacquet J M, Picco G P, eds. Coordination Models and Languages. Lect Notes in Comput Sci, Vol 3454. Beilin: Springer-Verlag, 2005. 1\u201316"},{"key":"6_CR11","series-title":"Lect Notes in Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-59450-7_9","volume-title":"Object-Based Models and Languages for Concurrent Systems","author":"N. Nierstrasz","year":"1995","unstructured":"Nierstrasz N, Meijler T D. Requirements for a composition language. In Ciancarini P, Nierstrasz O, Yonezawa A, eds. Object-Based Models and Languages for Concurrent Systems. Lect Notes in Comput Sci, Vol 924. Beilin: Springer-Verlag, 1995. 147\u2013161"},{"key":"6_CR12","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1109\/ICWS.2004.1314722","volume-title":"Proc. IEEE Int. Conf. on Web Services","author":"G. Salaun","year":"2004","unstructured":"Salaun G, Bordeaux L, Schaerf M. Describing and reasoning on web services using process algebra. In: Zhang L J, Jain H, Liu L, eds. Proc. IEEE Int. Conf. on Web Services. CA: IEEE Press, 2004. 43\u201350"},{"issue":"1","key":"6_CR13","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1023\/A:1024000426962","volume":"1","author":"E. Deelman","year":"2003","unstructured":"Deelman E, Blythe J, Gil Y, et al. Mapping abstract complex workflows onto grid environments. J Grid Comput, 2003, 1(1): 25\u201339","journal-title":"J Grid Comput"},{"key":"6_CR14","first-page":"676","volume-title":"Proc. IEEE Int. Symp. on Cluster Computing and the Grid. Vol. 2","author":"T. Fahringer","year":"2005","unstructured":"Fahringer T, Qin J, Hainzer S. Specification of grid workflow applications with AGWL: An abstract grid workflow language. In: Walker D W, Kesselman C, eds. Proc. IEEE Int. Symp. on Cluster Computing and the Grid. Vol. 2. UK: IEEE Press, 2005. 676\u2013685"},{"key":"6_CR15","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1109\/ICWS.2004.1314782","volume-title":"Proc. IEEE Int. Conf. on Web Services","author":"Y. Long","year":"2004","unstructured":"Long Y, Lam H, Su Y W. Adaptive grid service flow management: Framework and model. In: Zhang L J, Jain H, Liu L, eds. Proc. IEEE Int. Conf. on Web Services. CA: IEEE Press, 2004. 558\u2013565"},{"key":"6_CR16","series-title":"Lect Notes in Comput Sci","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-540-28642-4_18","volume-title":"Grid Computing","author":"S. Pllana","year":"2004","unstructured":"Pllana S, Fahringer T, Testori J, et al. Towards an UML based graphical representation of grid workflow applications. In: Dikaiakos M D, ed. Grid Computing. Lect Notes in Comput Sci, Vol 3165. Beilin: Springer-Verlag, 2004. 149\u2013158"},{"key":"6_CR17","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/j.jvlc.2004.08.004","volume":"16","author":"C. Pautasso","year":"2005","unstructured":"Pautasso C, Alonso G. The JOpera visual composition language. J Visual Lang Comput, 2005, 16: 119\u2013152","journal-title":"J Visual Lang Comput"},{"key":"6_CR18","first-page":"348","volume-title":"Proc. Int. Conf. on Information Technology: Coding and Computing","author":"P. Amnuaykanjanasin","year":"2005","unstructured":"Amnuaykanjanasin P, Nupairoj N. The BPEL orchestrating framework for secured grid services. In: Selvaraj H, ed. Proc. Int. Conf. on Information Technology: Coding and Computing. CA: IEEE Press, 2005. 348\u2013353"},{"issue":"4","key":"6_CR19","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1360\/122004-30","volume":"48","author":"S. H. Qing","year":"2005","unstructured":"Qing S H, Li G C. A formal model of fair exchange protocols. Sci China Ser F-Inf Sci, 2005, 48(4): 499\u2013512","journal-title":"Sci China Ser F-Inf Sci"},{"issue":"4","key":"6_CR20","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1360\/122004-78","volume":"48","author":"K. L. Su","year":"2005","unstructured":"Su K L, Lu G F, Chen Q L. Knowledge structure approach to verification of authentication protocols. Sci China Ser F-Inf Sci, 2005, 48(4): 513\u2013532","journal-title":"Sci China Ser F-Inf Sci"},{"key":"6_CR21","first-page":"127","volume-title":"Proc. 3rd IEEE Int. Conf. on Software Engineering and Formal Methods","author":"Z. N\u00e9meth","year":"2005","unstructured":"N\u00e9meth Z, P\u00e9rez C, Priol T. Workflow enactment based on a chemical metaphor. In: Aichernig B K, Beckert B, eds. Proc. 3rd IEEE Int. Conf. on Software Engineering and Formal Methods. CA: IEEE Press, 2005. 127\u2013136"},{"key":"6_CR22","series-title":"Lect Notes in Comput Sci","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"Chaki S, Clarke E M, Ouaknine J, et al. State \/ event-based software model checking. In Boiten E A, Derrick J, Smith G, eds. Integrated Formal Methods. Lect Notes in Comput Sci, Vol 2999. Beilin: Springer-Verlag, 2004. 128\u2013147"},{"key":"6_CR23","first-page":"257","volume-title":"Proc. 11th ACM SIGSOFT Int. Symp. on Foundations of Software Engineering","author":"D. Giannakopoulou","year":"2003","unstructured":"Giannakopoulou D, Magee J. Fluent model checking for event-based systems. In: Paakki J, ed. Proc. 11th ACM SIGSOFT Int. Symp. on Foundations of Software Engineering. NY: ACM Press, 2003. 257\u2013266"},{"key":"6_CR24","first-page":"97","volume-title":"Proc. 9th IEEE Conference on Engineering Complex Computer Systems","author":"K. Taguchi","year":"2004","unstructured":"Taguchi K, Dong J S, Ciobanu G. Relating Pi calculus to Object-Z. In: Bellini P, Bohner S, Steffen B, ed. Proc. 9th IEEE Conference on Engineering Complex Computer Systems. CA: IEEE Press, 2004. 97\u2013106"},{"issue":"2","key":"6_CR25","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. D. Nicola","year":"1995","unstructured":"Nicola R D, Vaandrager F. Three logics for branching bisimulation. JACM, 1995, 42(2): 458\u2013487","journal-title":"JACM"},{"key":"6_CR26","first-page":"49","volume-title":"Communicating and Mobile Systems: the Pi-calculus","author":"R. Milner","year":"1999","unstructured":"Milner R. Communicating and Mobile Systems: the Pi-calculus. Cambridge: Cambridge University Press, 1999. 49\u201350"},{"issue":"2","key":"6_CR27","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1023\/A:1008645826258","volume":"12","author":"B. Cinzia","year":"1998","unstructured":"Cinzia B, Alessandro F, Stefania G, et al. A formal verification environment for railway signaling system design. Form Method Syst Des, 1998, 12(2): 139\u2013161","journal-title":"Form Method Syst Des"},{"key":"6_CR28","series-title":"Lect Notes in Comput Sci","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Veriifcation","author":"A. Cimatti","year":"2002","unstructured":"Cimatti A, Clarke E, Giunchiglia E, et al. NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma E, Larsen K G, eds. Computer Aided Veriifcation. Lect Notes in Comput Sci, Vol 2404. Beilin: Springer-Verlag, 2002. 359\u2013364"},{"issue":"11","key":"6_CR29","doi-asserted-by":"crossref","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C. Heitmeyer","year":"1998","unstructured":"Heitmeyer C, Kirby J, Labaw B, et al. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE T Software Eng, 1998, 24(11): 927\u2013948","journal-title":"IEEE T Software Eng"},{"key":"6_CR30","first-page":"28","volume-title":"Proc. 5th Int. Conf. on Grid and Cooperative Computing","author":"K. Xu","year":"2006","unstructured":"Xu K, Wang Y X, Wu C. Aspect oriented region analysis for efficient grid application reasoning. In: Xiao N, Rajkumar B, Liu Y H, eds. Proc. 5th Int. Conf. on Grid and Cooperative Computing. CA: IEEE Press, 2006. 28\u201331"},{"key":"6_CR31","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1145\/302405.302672","volume-title":"Proc. 21th Int. Conf. on Software Engineering","author":"M. B. Dwyer","year":"1999","unstructured":"Dwyer M B, Avrunin G S, Corbett J C. Patterns in property specifications for finite-state verification. In: Boehm B, Garlan D, Kramer J, eds. Proc. 21th Int. Conf. on Software Engineering. CA: IEEE Press, 1999. 411\u2013431"}],"container-title":["Science in China Series F: Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-007-0006-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-007-0006-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-007-0006-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T18:15:00Z","timestamp":1683915300000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-007-0006-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,2]]}},"alternative-id":["6"],"URL":"https:\/\/doi.org\/10.1007\/s11432-007-0006-9","relation":{},"ISSN":["1009-2757","1862-2836"],"issn-type":[{"value":"1009-2757","type":"print"},{"value":"1862-2836","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2]]}}}