{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T06:00:51Z","timestamp":1774332051258,"version":"3.50.1"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,9,1]],"date-time":"2011-09-01T00:00:00Z","timestamp":1314835200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2011,9]]},"DOI":"10.1007\/s11334-011-0172-1","type":"journal-article","created":{"date-parts":[[2011,10,6]],"date-time":"2011-10-06T07:36:40Z","timestamp":1317886600000},"page":"209-224","source":"Crossref","is-referenced-by-count":3,"title":["Algebraic approach to linking the semantics of web services"],"prefix":"10.1007","volume":"7","author":[{"given":"Huibiao","family":"Zhu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jifeng","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jing","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan P.","family":"Bowen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,10,7]]},"reference":[{"key":"172_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial J-R (1996) The B-book: assigning programs to meanings. University Press, Cambridge"},{"issue":"2","key":"172_CR2","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1006\/inco.1996.0056","volume":"127","author":"SD Brookes","year":"1996","unstructured":"Brookes SD (1996) Full abstraction for a shared-variable parallel language. Inf Comput 127(2): 145\u2013163","journal-title":"Inf Comput"},{"key":"172_CR3","doi-asserted-by":"crossref","unstructured":"Bruni R, Ferrari GL, Melgratti HC, Montanari U, Strollo D, Tuosto E (2005) From theory to practice in transactional composition of web services. In: Proceedings of EPEW\/WS-FM 2005: European performance engineering workshop and international workshop on web services and formal methods, Versailles, France, September 1\u20133, 2005. Lecture notes in computer science, vol 3670. Springer, Berlin, pp 272\u2013286","DOI":"10.1007\/11549970_20"},{"key":"172_CR4","unstructured":"Bruni R, Melgratti HC, Montanari U (2004) Theoretical foundations for compensations in flow composition languages. In: Proceedings of POPL 2005: 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, Long Beach, California, USA, January 12\u201314, 2005. ACM, USA, pp 209\u2013220"},{"key":"172_CR5","doi-asserted-by":"crossref","unstructured":"Butler M, Ripon S (2005) Executable semantics for compensating CSP. In: Proceedings of EPEW 2005: international workshop on web services and formal methods, Versailles, France, September 1\u20133, 2005. Lecture notes in computer science, vol 3670. Springer, Berlin, pp 243\u2013256","DOI":"10.1007\/11549970_18"},{"key":"172_CR6","unstructured":"Butler MJ, Ferreira C (2000) A process compensation language. In: Proceedings of IFM 2000: 2nd international conference on integrated formal methods, Dagstuhl Castle, Germany, November 1\u20133, 2000. Lecture notes in computer science, vol 1945. Springer, Berlin, pp 61\u201376"},{"key":"172_CR7","unstructured":"Butler MJ, Ferreira C (2004) An operational semantics for StAC, a language for modelling long-running business transactions. In: COORDINATION 2004: 6th international conference on coordination models and languages, Pisa, Italy, February 24\u201327, 2004. Lecture notes in computer science, vol 2949. Springer, Berlin, pp 87\u2013104"},{"issue":"5","key":"172_CR8","first-page":"712","volume":"11","author":"MJ Butler","year":"2005","unstructured":"Butler MJ, Ferreira C, Ng MY (2005) Precise modelling of compensating business transactions and its application to BPEL. J Univers Comput Sci 11(5): 712\u2013743","journal-title":"J Univers Comput Sci"},{"key":"172_CR9","doi-asserted-by":"crossref","unstructured":"Butler MJ, Hoare CAR, Ferreira C (2005) A trace semantics for long-running transactions. In: Communicating sequential processes: the first 25\u00a0years, symposium on the occasion of 25\u00a0years of CSP, London, UK, July 7\u20138, 2004. Lecture notes in computer science, vol 3525. Springer, Berlin, pp 133\u2013150","DOI":"10.1007\/11423348_8"},{"key":"172_CR10","unstructured":"Cerone A, Zhao X, Krishnan P (2006) Modelling and resource allocation planning of BPEL workflows under security constraints. Technical report 336, UNU\/IIST, P.O. Box 3058, Macau SAR, China, June"},{"key":"172_CR11","unstructured":"Curbera F, Goland Y, Klein J, Leymann F, Roller D, Satish Thatte M, Weerawarana S (2003) Business process execution language for web service. http:\/\/www.siebel.com\/bpel"},{"key":"172_CR12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569760","volume-title":"Specification and proof in real-time CSP","author":"J Davis","year":"1993","unstructured":"Davis J (1993) Specification and proof in real-time CSP. University Press, Cambridge"},{"key":"172_CR13","unstructured":"de Bakker J, de Vink E (1996) Control flow semantics. MIT Press, Massachusetts"},{"key":"172_CR14","unstructured":"Dijkstra EW (1976) A discipline of programming. Prentice Hall International Series in Automatic Computation"},{"key":"172_CR15","doi-asserted-by":"crossref","unstructured":"Garcia-Molina H, Salem K (1987) Sagas. In: Proceedings of ACM SIGMOD international conference on management of data, San Francisco, California, USA, May 27\u201329, 1987. ACM, USA, pp 249\u2013259","DOI":"10.1145\/38713.38742"},{"key":"172_CR16","doi-asserted-by":"crossref","unstructured":"Glabbeek Rv (1993) The linear time\u2014branching time spectrum II; the semantics of sequential systems with silent moves (extended abstract). In: Best E (ed) Proceedings of CONCUR\u201993: 4th international conference on concurrency theory, Hildesheim, Germany, August 1993. Lecture notes in computer science, vol 715. Springer, Berlin, pp 66\u201381","DOI":"10.1007\/3-540-57208-2_6"},{"key":"172_CR17","unstructured":"Glabbeek Rv (1996) Comparative Concurrency Semantics and Refinement of Actions. CWI Tract, vol 109. CWI, Amsterdam (Second edition of dissertation)"},{"key":"172_CR18","unstructured":"Glabbeek Rv (2001) The linear time\u2014branching time spectrum I; the semantics of concrete, sequential processes. In: Bergstra J, Ponse A, Smolka S (eds) Handbook of process algebra, chapt 1. Elsevier, Amsterdam, pp 3\u201399"},{"key":"172_CR19","unstructured":"He J (2008) Modelling coordination and compensation. In: Proceedings of ISoLA 2008: 3rd international symposium on leveraging applications of formal methods, verification and validation, Porto Sani, Greece, 13\u201315 October. Communications in Computer and Information Science, vol 17. Springer, Berlin, pp 15\u201336"},{"issue":"1","key":"172_CR20","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 (2007) A model for BPEL-like languages. Front Comput Sci China 1(1): 9\u201319","journal-title":"Front Comput Sci China"},{"issue":"8","key":"172_CR21","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare CAR (1978) Communicating sequential processes. Commun ACM 21(8): 666\u2013677","journal-title":"Commun ACM"},{"key":"172_CR22","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall International Series in Computer Science"},{"issue":"8","key":"172_CR23","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/27651.27653","volume":"38","author":"CAR Hoare","year":"1987","unstructured":"Hoare CAR, Hayes IJ, He J, Morgan C, Roscoe AW, Sanders JW, S\u00f8rensen IH, Spivey JM, Sufrin B (1987) Laws of programming. Commun ACM 38(8): 672\u2013686","journal-title":"Commun ACM"},{"key":"172_CR24","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/0020-0190(93)90219-Y","volume":"45","author":"CAR Hoare","year":"1993","unstructured":"Hoare CAR, He J (1993) From algebra to operational semantics. Inf Process Lett 45: 75\u201380","journal-title":"Inf Process Lett"},{"key":"172_CR25","unstructured":"Hoare CAR, He J (1998) Unifying theories of programming. Prentice Hall International Series in Computer Science"},{"key":"172_CR26","unstructured":"Hoare CAR, Jifeng H, Sampaio A (1997) Algebraic derivation of an operational semantics. In: Plotkin G, Stirling C, Tofte M (eds) Proof, language and interaction: essays in honour of Robin Milner, foundations of computer science series. The MIT Press, Massachusetts"},{"issue":"5","key":"172_CR27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1022494.1022526","volume":"29","author":"M Koshkina","year":"2004","unstructured":"Koshkina M, van Breugel F (2004) Modelling and verifying web service orchestration by means of the concurrency workbench. ACM SIGSOFT Softw Eng Notes 29(5): 1\u201310","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"172_CR28","unstructured":"Laneve C, Zavattaro G (2005) Web-pi at work. In: Proceedings of TGC 2005: international symposium on trustworthy global computing, Edinburgh, UK, April 7\u20139, 2005. Lecture notes in computer science, vol 3705. Springer, Berlin, pp 182\u2013194"},{"issue":"2\u20133","key":"172_CR29","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1016\/j.scico.2008.07.001","volume":"73","author":"R Lanotte","year":"2008","unstructured":"Lanotte R, Maggiolo-Schettini A, Milazzo P, Troina A (2008) Design and verification of long-running transactions in a timed framework. Sci Comput Program 73(2\u20133): 76\u201394","journal-title":"Sci Comput Program"},{"key":"172_CR30","unstructured":"Leymann F (2001) Web Services Flow Language (WSFL 1.0). IBM http:\/\/www-3.ibm.com\/software\/solutions\/webservices\/pdf\/WSDL.pdf"},{"key":"172_CR31","doi-asserted-by":"crossref","unstructured":"Li J, Zhu H, Pu G, He J (2007) Looking into compensable transactions. In: Proceedings of SEW-31: 31st IEEE software engineering workshop, Baltimore, USA. IEEE Computer Society Press, Los Angeles, pp 154\u2013166","DOI":"10.1109\/SEW.2007.62"},{"issue":"1","key":"172_CR32","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/j.jlap.2006.05.007","volume":"70","author":"R Lucchi","year":"2007","unstructured":"Lucchi R, Mazzara M (2007) A pi-calculus based semantics for ws-bpel. J Log Algebraic Program 70(1): 96\u2013118","journal-title":"J Log Algebraic Program"},{"key":"172_CR33","doi-asserted-by":"crossref","unstructured":"Luo C, Qin S, Qiu Z (2008) Verifying bpel-like programs with hoare logic. In: Proceedings of TASE 2008: 2nd IEEE international symposium on theoretical aspects of software engineering, Nanjing, China, June 2008. IEEE Computer Society, Los Angeles, pp 151\u2013158","DOI":"10.1109\/TASE.2008.41"},{"issue":"4","key":"172_CR34","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1007\/s11704-008-0039-2","volume":"2","author":"C Luo","year":"2008","unstructured":"Luo C, Qin S, Qiu Z (2008) Verifying bpel-like programs with hoare logic. Front Comput Sci China 2(4): 344\u2013356","journal-title":"Front Comput Sci China"},{"key":"172_CR35","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"172_CR36","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"172_CR37","unstructured":"McIver A, Morgan C (2004) Abstraction, refinement and proof of probability systems. monographs in computer science. Springer, Berlin"},{"key":"172_CR38","volume-title":"Communication and mobile system: \u03c0-calculus","author":"R Milner","year":"1999","unstructured":"Milner R (1999) Communication and mobile system: \u03c0-calculus. University Press, Cambridge"},{"key":"172_CR39","unstructured":"Moss J (1981) Nested transactions: an approach to reliable distributed computing. PhD thesis, Department of Electrical Engineering and Computer Science, MIT, April"},{"key":"172_CR40","unstructured":"Plotkin G (2004) A structural approach to operational semantics. Technical report 19, University of Aahus, 1981. J Log Algebraic Program 60\u201361:17\u2013139"},{"issue":"2","key":"172_CR41","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/j.entcs.2005.07.035","volume":"151","author":"G Pu","year":"2006","unstructured":"Pu G, Zhao X, Wang S, Qiu Z (2006) Towards the semantics and verification of BPEL4WS. Electron Notes Theor Comput Sci 151(2): 33\u201352","journal-title":"Electron Notes Theor Comput Sci"},{"key":"172_CR42","unstructured":"Pu G, Zhu H, Qiu Z, Wang S, Zhao X, He J (2006) Theoretical foundations of scope-based compensation flow language for web service. In: Proceedings of FMOODS 2005: 8th IFIP international conference on formal methods for open object-based distributed systems, Bologna, Italy, 14\u201316 June, 2006. Lecture notes in computer science, vol 4307. Springer, Berlin, pp 251\u2013266."},{"key":"172_CR43","doi-asserted-by":"crossref","unstructured":"Qiu Z, Wang S, Pu G, Zhao X (2005) Semantics of BPEL4WS-Like fault and compensation handling. In: Proceedings of FM 2005: international symposium of formal methods Europe, Newcastle, UK, July 18\u201322, 2005. Lecture notes in computer science, vol 3582. Springer, Berlin, pp 350\u2013365","DOI":"10.1007\/11526841_24"},{"key":"172_CR44","unstructured":"Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall International Series in Computer Science"},{"key":"172_CR45","unstructured":"Scott D, Strachey C (1971) Towards a mathematical semantics for computer languages. Technical report PRG-6, Oxford University Computer Laboratory"},{"key":"172_CR46","unstructured":"Thatte S (2001) XLANG: Web Service for Business Process Design. Microsoft, http:\/\/www.gotdotnet.com\/team\/xml_wsspecs\/xlang-c\/default.html"},{"key":"172_CR47","doi-asserted-by":"crossref","unstructured":"van Breugel F, Koshkina M (2005) Dead-path-elimination in bpel4ws. In: Proceedings of ACSD 2005: fifth international conference on application of concurrency to system design, pp 192\u2013201, St. Malo, France, June, IEEE Computer Society, Los Angeles","DOI":"10.1109\/ACSD.2005.11"},{"key":"172_CR48","unstructured":"Zhu H (2005) Linking the semantics of a multithreaded discrete event simulation language. PhD thesis, London, South Bank University, February"},{"key":"172_CR49","unstructured":"Zhu H, Bowen JP, He J (2002) Soundness, completeness and non-redundancy of operational semantics for Verilog based on denotational semantics. In: Proceedings of ICFEM 2002: 4th international conference on formal engineering methods. Lecture notes in computer science, vol 2495. Springer, Berlin, pp 600\u2013612"},{"key":"172_CR50","unstructured":"Zhu H, He J (2000) A semantics of Verilog using duration calculus. In: Proceedings of international conference on software: theory and practice, pp 421\u2013432"},{"key":"172_CR51","unstructured":"Zhu H, He J, Bowen JP (2006) From operational semantics to denotational semantics for Verilog. In: Proceedings of ICECCS 2006: 11th IEEE international conference on engineering of complex computer systems. IEEE Computer Society Press, Los Angeles, pp 139\u2013151"},{"key":"172_CR52","doi-asserted-by":"crossref","unstructured":"Zhu H, He J, Li J (2007) Unifying denotational semantics with operational semantics for web services. In: Proceedings of ICDCIT 2007: 4th international conference on distributed computing and internet technology, Bangalore, India, 17\u201320 December. Lecture notes in computer science, vol 4882. Springer, Berlin, pp 225\u2013239","DOI":"10.1007\/978-3-540-77115-9_23"},{"key":"172_CR53","doi-asserted-by":"crossref","unstructured":"Zhu H, He J, Li J, Bowen JP (2007) Algebraic approach to linking the semantics of web services. In: Proceedings of SEFM 2007: 5th IEEE international conference on software engineering and formal methods. IEEE Computer Society Press, Los Angeles, pp 315\u2013326","DOI":"10.1109\/SEFM.2007.4"},{"key":"172_CR54","doi-asserted-by":"crossref","unstructured":"Zhu H, He J, Pu G, Li J (2007) An operational approach to BPEL-like programming. In: Proceedings of SEW-31: 31st IEEE software engineering workshop, Baltimore, USA. IEEE Computer Society Press, Los Angeles, pp 236\u2013245","DOI":"10.1109\/SEW.2007.56"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-011-0172-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-011-0172-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-011-0172-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T14:27:59Z","timestamp":1741789679000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-011-0172-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9]]},"references-count":54,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,9]]}},"alternative-id":["172"],"URL":"https:\/\/doi.org\/10.1007\/s11334-011-0172-1","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,9]]}}}