{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,5]],"date-time":"2025-02-05T03:40:10Z","timestamp":1738726810263,"version":"3.37.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T00:00:00Z","timestamp":1228089600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci. China"],"published-print":{"date-parts":[[2008,12]]},"DOI":"10.1007\/s11704-008-0039-2","type":"journal-article","created":{"date-parts":[[2008,12,4]],"date-time":"2008-12-04T06:10:17Z","timestamp":1228371017000},"page":"344-356","source":"Crossref","is-referenced-by-count":5,"title":["Verifying BPEL-like programs with Hoare logic"],"prefix":"10.1007","volume":"2","author":[{"given":"Chenguang","family":"Luo","sequence":"first","affiliation":[]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[]},{"given":"Zongyan","family":"Qiu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,12,5]]},"reference":[{"key":"39_CR1","unstructured":"Thatte S. XLANG: web service for business process design. http:\/\/www.gotdotnet.com\/team\/xml_wsspecs\/xlang-c\/default.htm , Microsoft, 2001"},{"key":"39_CR2","unstructured":"Leymann F. WSFL: web service flow language. http:\/\/www-4.ibm.com\/software\/solutions\/webservices\/pdf\/WSFL.pdf , IBM, 2001"},{"key":"39_CR3","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-540-24634-3_9","volume":"2949","author":"M. Butler","year":"2004","unstructured":"Butler M, Ferreira C. An operational semantics for StAC, a language for modelling long-running business transactions. In: Proceedings of the 6th International Conference on Coordination Models and Languages, Lecture Notes in Computer Science, Vol 2949, Springer, 2004, 87\u2013104","journal-title":"Proceedings of the 6th International Conference on Coordination Models and Languages, Lecture Notes in Computer Science"},{"key":"39_CR4","unstructured":"Alves A, Arkin A, Askary S, et al. web service business process execution language version 2.0. http:\/\/docs.oasis-open.org\/wsbpel\/2.0\/OS\/wsbpel-v2.0-OS.html , OASIS Standard, 2007"},{"key":"39_CR5","unstructured":"Barreto C, Bullard V, Erl T, et al. web service business process execution language version 2.0 primer. http:\/\/docs. oasis-open.org\/wsbpel\/2.0\/Primer\/wsbpel-v2.0-Primer.html , OASIS Standard, 2007"},{"key":"39_CR6","doi-asserted-by":"crossref","unstructured":"Qiu Z, Wang S, Pu G et al. Semantics of bpel4ws-like fault and compensation handing. In: Proceedings of the 1st International Symposium of Formal Methods Europe, Lecture Notes in Computer Science, Vol 3582, Springer, 2005, 350\u2013365","DOI":"10.1007\/11526841_24"},{"key":"39_CR7","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/11768869_19","volume":"4037","author":"G. Pu","year":"2006","unstructured":"Pu G, Zhu H, Qiu Z et al. Theoretical foundation of scopebased compensable flow language for web service. In: Proceedings of the 1st International Conference on Formal Methods for Open Object-Based Distributed Systems, Lecture Notes in Computer Science, Vol 4037, Springer, 2006, 251\u2013266","journal-title":"Proceedings of the 1st International Conference on Formal Methods for Open Object-Based Distributed Systems"},{"key":"39_CR8","doi-asserted-by":"crossref","unstructured":"Qiu Z, Zhao X, Cai C et al. Towards the theoretical foundation of choreography. In: Proceedings of the 6th International World Wide Web Conference, ACM Press, 2007, 973\u2013982","DOI":"10.1145\/1242572.1242704"},{"issue":"1","key":"39_CR9","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/s11704-007-0002-7","volume":"1","author":"J. He","year":"2007","unstructured":"He J, Zhu H, Pu G. A model for bpel-like languages. Frontiers of Computer Science in China. 2007, 1(1):9\u201319","journal-title":"Frontiers of Computer Science in China"},{"key":"39_CR10","doi-asserted-by":"crossref","unstructured":"Zhu H, He J, Li J et al. Algebraic approach to linking the semantics of web services. In: Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Method, 2007, 315\u2013328","DOI":"10.1109\/SEFM.2007.4"},{"issue":"2","key":"39_CR11","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q. Xu","year":"1997","unstructured":"Xu Q, de Roever W P, He J. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 1997, 9(2): 149\u2013174","journal-title":"Formal Aspects of Computing"},{"key":"39_CR12","unstructured":"Zhu H. Linking the semantics of a multithreaded discrete event simulation language. Dissertation for the Doctoral Degree. London South Bank University, 2005"},{"key":"39_CR13","unstructured":"Fowler M, Scott K. UML distilled: a brief guide to the standard object modeling language. Addison-Wesley, 2000"},{"key":"39_CR14","doi-asserted-by":"crossref","unstructured":"Garcia-Molina H, Salem K. Sagas. In: Proceedings of the Association for Computing Machinery Special Interest Group on Management of Data Conference, ACM Press, 1987, 249\u2013259","DOI":"10.1145\/38713.38742"},{"key":"39_CR15","unstructured":"Moss J. Nested transactions: an approach to reliable distributed computing. Dissertation for the Doctoral Degree. Massachusetts Institute of Technology, 1981"},{"key":"39_CR16","first-page":"200","volume":"2813","author":"W. Analst","year":"2003","unstructured":"Analst W, Dumas M, Hofstede A, et al. Analysis of web services composition languages: the case of bpel4ws. In: Proceedings of the 22nd International Conference on Conceptual Modeling, Lecture Notes in Computer Science, Vol 2813. Springer, 2003, 200\u2013215","journal-title":"Proceedings of the 22nd International Conference on Conceptual Modeling"},{"key":"39_CR17","first-page":"191","volume":"47","author":"R. Hamadi","year":"2003","unstructured":"Hamadi R, Benatallah B. A petri net-based model for web service composition. In: Proceedings of the 14th Australasian Database Conference, Vol 47, Adelaide, Australia, 2003, 191\u2013200","journal-title":"Proceedings of the 14th Australasian Database Conference"},{"key":"39_CR18","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/j.entcs.2004.05.007","volume":"105","author":"A. Brogi","year":"2004","unstructured":"Brogi A, Canal C, Pimentel E et al. Formalizing web service choreographies. Electronic Notes in Theoretical Computer Science, 2004, 105: 73\u201394","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"39_CR19","unstructured":"Andrews T, Curbera F, Dholakia H, et al. Business process execution language for web services 1.1. http:\/\/download.boulder.ibm.com\/ibmdl\/pub\/software\/dw\/specs\/WS-bpel.pdf , 2003"},{"key":"39_CR20","doi-asserted-by":"crossref","unstructured":"Bruni R, Melgratti H, Montanari U. Theoretical foundations for compensations in flow composition languages. In: Proceedings of the 32nd SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), New York, USA, 2005, 209\u2013220","DOI":"10.1145\/1040305.1040323"},{"key":"39_CR21","doi-asserted-by":"crossref","unstructured":"Duan Z, Bernstein A, Lewis P et al. Semantics based verification and synthesis of bpel4ws abstract processes. In: Proceedings of the IEEE International Conference on Web Services, 2004, 734\u2013737","DOI":"10.1109\/ICWS.2004.1314805"},{"key":"39_CR22","doi-asserted-by":"crossref","unstructured":"Duan Z, Bernstein A, Lewis P et al. A model for abstract process specification, verification and composition. In: Proceedings of the 2nd International Conference on Service Oriented Computing, New York, USA, 2004, 232\u2013241","DOI":"10.1145\/1035167.1035201"},{"key":"39_CR23","doi-asserted-by":"crossref","unstructured":"Fu X, Bultan T, Su J. Analysis of interacting bpel web services. In: Proceedings of the 13th International World Wide Web Conference, ACM Press, 2004, 621\u2013630","DOI":"10.1145\/988672.988756"},{"key":"39_CR24","unstructured":"Holzmann G. The spin model checker:primer and reference manual. Addison-Wesley, 2003"},{"key":"39_CR25","doi-asserted-by":"crossref","unstructured":"Pu G, Zhao S, Wang S. Towards the semantics and verification of bpel4ws. In: Proceedings of the International Workshop on Web Languages and Formal Methods (WLFM), Electronic Notes in Theoretical Computer Science, Vol 151, Elsevier, 2005, 33\u201352","DOI":"10.1016\/j.entcs.2005.07.035"},{"key":"39_CR26","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Proceedings of the DIMACS\/SYCON Workshop on Hybrid Systems III: Verification and Control","author":"J. Bengtsson","year":"1996","unstructured":"Bengtsson J, Larsen K, Larsson F, et al. Uppaal-a tool suitable for automatic verification of real-time systems. In: Proceedings of the DIMACS\/SYCON Workshop on Hybrid Systems III: Verification and Control, Secaucus, New Jersey, USA, New York: Springer, 1996, 232\u2013243"}],"container-title":["Frontiers of Computer Science in China"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-008-0039-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-008-0039-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-008-0039-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,5]],"date-time":"2025-02-05T02:55:21Z","timestamp":1738724121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-008-0039-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12]]},"references-count":26,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["39"],"URL":"https:\/\/doi.org\/10.1007\/s11704-008-0039-2","relation":{},"ISSN":["1673-7350","1673-7466"],"issn-type":[{"type":"print","value":"1673-7350"},{"type":"electronic","value":"1673-7466"}],"subject":[],"published":{"date-parts":[[2008,12]]}}}