{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,8]],"date-time":"2023-09-08T00:05:18Z","timestamp":1694131518548},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2010,4,30]],"date-time":"2010-04-30T00:00:00Z","timestamp":1272585600000},"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":[[2010,12]]},"DOI":"10.1007\/s11334-010-0134-z","type":"journal-article","created":{"date-parts":[[2010,4,29]],"date-time":"2010-04-29T04:22:00Z","timestamp":1272514920000},"page":"283-298","source":"Crossref","is-referenced-by-count":3,"title":["Linking denotational semantics with operational semantics for web services"],"prefix":"10.1007","volume":"6","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":"Geguang","family":"Pu","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":[[2010,4,30]]},"reference":[{"key":"134_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. Cambridge University Press, Cambridge"},{"issue":"2","key":"134_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":"134_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":"134_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, New York, pp 209\u2013220"},{"key":"134_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":"134_CR6","doi-asserted-by":"crossref","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","DOI":"10.1007\/3-540-40911-4_5"},{"key":"134_CR7","unstructured":"Butler MJ, Ferreira C (2004) An operational semantics for StAC, a language for modelling long-running business transactions. In: Proceedings of 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"},{"key":"134_CR8","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":"134_CR9","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 Comp Sci 11(5): 712\u2013743","journal-title":"J Univers Comp Sci"},{"key":"134_CR10","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":"134_CR11","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 2006"},{"key":"134_CR12","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":"134_CR13","volume-title":"Control flow semantics","author":"J Bakker de","year":"1996","unstructured":"de Bakker J, de Vink E (1996) Control flow semantics. The MIT Press, London"},{"issue":"2","key":"134_CR14","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev D, Yao AC (1983) On the security of public key protocols. IEEE Trans Inf Theory 29(2): 198\u2013207","journal-title":"IEEE Trans Inf Theory"},{"key":"134_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, New York, pp 249\u2013259","DOI":"10.1145\/38713.38742"},{"issue":"1","key":"134_CR16","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 Comp Sci China 1(1): 9\u201319","journal-title":"Front Comp Sci China"},{"issue":"8","key":"134_CR17","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":"134_CR18","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall international series in computer science"},{"issue":"8","key":"134_CR19","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":"134_CR20","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":"134_CR21","unstructured":"Hoare CAR, He J (1998) Unifying theories of programming. Prentice Hall international series in computer science"},{"key":"134_CR22","volume-title":"Proof, language and interaction: essays in honour of Robin Milner, Foundations of Computer Science series","author":"CAR Hoare","year":"1997","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, London"},{"key":"134_CR23","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"},{"key":"134_CR24","unstructured":"Leymann F (2001) Web services flow language (WSFL 1.0) IBM, 2001. http:\/\/www-3.ibm.com\/software\/solutions\/webservices\/pdf\/WSDL.pdf"},{"key":"134_CR25","unstructured":"Li J (2008) Web transaction modeling and its semantic analysis (in Chinese). PhD thesis, Software Engineering Institute, East China Normal University, China, June 2008"},{"key":"134_CR26","doi-asserted-by":"crossref","unstructured":"Li J, He J, Pu G, Zhu H (2006) Towards the semantics for web services choreography description language. In: Proceedings of ICFEM 2006: 8th international conference on formal engineering methods, Macau, China, 29 October\u20133 November, 2006. Lecture notes in computer science, vol 4260. Springer, Berlin, pp 246\u2013 263","DOI":"10.1007\/11901433_14"},{"key":"134_CR27","doi-asserted-by":"crossref","unstructured":"Li J, Zhu H, He J (2007) Algebraic semantics for compensable transactions. In: Proceedings of ICTAC 2007: 4th international colloquium on theoretical aspects of computing, Macau, China, 26\u201328 September, 2007. Lecture notes in computer science, vol 4711. Springer, Berlin, pp 306\u2013321","DOI":"10.1007\/978-3-540-75292-9_21"},{"key":"134_CR28","doi-asserted-by":"crossref","unstructured":"Li J, Zhu H, He J (2008) An observational model for transactional calculus of services orchestration. In: Proceedings of ICTAC 2008: 5th international colloquium on theoretical aspects of computing, Istanbul, Turkey, 1\u20133 September, 2008. Lecture notes in computer science, vol 5048. Springer, Berlin, pp 149\u2013168","DOI":"10.1007\/978-3-540-85762-4_14"},{"key":"134_CR29","doi-asserted-by":"crossref","unstructured":"Li J, Zhu H, Pu G, JH (2007) A formal model for compensable transactions. In: Proceedings of ICECCS 2007: 12th IEEE international conference on engineering of complex computer systems. IEEE Computer Society Press, pp 64\u201373","DOI":"10.1109\/ICECCS.2007.8"},{"key":"134_CR30","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, pp 154\u2013166","DOI":"10.1109\/SEW.2007.62"},{"issue":"1","key":"134_CR31","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 Logic Algebraic Program 70(1): 96\u2013118","journal-title":"J Logic Algebraic Program"},{"key":"134_CR32","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, pp 151\u2013158","DOI":"10.1109\/TASE.2008.41"},{"key":"134_CR33","volume-title":"Abstraction, refinement and proof of probability systems. Monographs in Computer Science","author":"A McIver","year":"2004","unstructured":"McIver A, Morgan C (2004) Abstraction, refinement and proof of probability systems. Monographs in Computer Science. Springer, Berlin"},{"key":"134_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A calculus of communicating systems. Lecture Notes in Computer Science, vol 18","author":"R Milner","year":"1980","unstructured":"Milner R (1980) A calculus of communicating systems. Lecture Notes in Computer Science, vol 18. Springer, Berlin"},{"key":"134_CR35","unstructured":"Milner R (1990) Communication and concurrency. Prentice Hall International Series in Computer Science"},{"key":"134_CR36","volume-title":"Communication and mobile system: \u03c0-calculus","author":"R Milner","year":"1999","unstructured":"Milner R (1999) Communication and mobile system: \u03c0-calculus. Cambridge University Press, Cambridge"},{"key":"134_CR37","doi-asserted-by":"crossref","unstructured":"Montangero C, Semini L (2006) A logical view of choreography. In: Proceedings of COORDINATION 2006: 8th international conference on coordination models and languages, Bologna, Italy, June 14\u201316, 2006. Lecture notes in computer science, vol 4038. Springer, Berlin, pp 179\u2013193","DOI":"10.1007\/11767954_12"},{"key":"134_CR38","unstructured":"Moss J (1981) Nested transactions: an approach to reliable distributed computing. PhD thesis, Department of Electrical Engineering and Computer Science, MIT, April 1981"},{"key":"134_CR39","doi-asserted-by":"crossref","unstructured":"Plotkin G (2004) A structural approach to operational semantics. Technical Report 19, University of Aahus, 1981. (Also published in J Logic Algebraic Program 60\u201361:17\u2013139)","DOI":"10.1016\/j.jlap.2004.05.001"},{"issue":"2","key":"134_CR40","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. Electr Notes Theoret Comp Sci 151(2): 33\u201352","journal-title":"Electr Notes Theoret Comp Sci"},{"key":"134_CR41","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":"134_CR42","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":"134_CR43","unstructured":"Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall International Series in Computer Science"},{"key":"134_CR44","unstructured":"Thatte S (2001) XLANG: web service for business process design. Microsoft. http:\/\/www.gotdotnet.com\/team\/xml_wsspecs\/xlang-c\/default.html"},{"key":"134_CR45","unstructured":"WS-CDL. http:\/\/www.w3.org\/TR\/ws-cdl-10\/"},{"key":"134_CR46","doi-asserted-by":"crossref","unstructured":"Yang H, Cai C, Peng L, Zhao X, Qiu Z (2008) Reasoning about channel passing in choreography. In: Proceedings of TASE 2008: 2nd IEEE international symposium on theoretical aspects of software engineering, Nanjing, China, June 2008. IEEE Computer Society, pp 135\u2013142","DOI":"10.1109\/TASE.2008.19"},{"key":"134_CR47","unstructured":"Yang H, Zhao X, Cai C, Qiu Z (2007) Exploring the connection of choreography and orchestration with exception handling and finalization\/compensation. In: Proceedings of 27th IFIP international conference on formal techniques for networked and distributed systems, Tallinn, Estonia, 27\u201329 June, 2007, Lecture notes in computer science, vol 4574. Springer, Berlin, pp 81\u201396"},{"key":"134_CR48","doi-asserted-by":"crossref","unstructured":"Yang H, Zhao X, Qiu Z, Cai C, Pu G (2006) Type checking choreography description language. In: Proceedings of ICFEM 2006: 8th international conference on formal engineering methods, Macau, China, 29 October\u20133 November, 2006, Lecture notes in computer science, vol 4260. Springer, Berlin","DOI":"10.1007\/11901433_15"},{"key":"134_CR49","unstructured":"Yang H, Zhao X, Qiu Z, Pu G, Wang S (2006) A formal model for web service choreography description language (WS-CDL). In: Proceedings of ICWS 2006: the 2006 IEEE international conference on web services. IEEE Computer Society Press, pp 893\u2013894"},{"key":"134_CR50","unstructured":"Zhao X, Cai C, Yang H, Qiu Z (2007) A QoS view of web service choreography. In: Proceedings of 3rd IEEE international workshop on service-oriented system engineering, Hong Kong, China, 2007. IEEE Computer Society"},{"key":"134_CR51","unstructured":"Zhao X, Yang H, Qiu Z (2006) Towards the formal model and verification of web service choreography description language. In: Proceedings of FM-WS 2006: 3rd international workshop on web services and formal methods, Vienna, Austria, 8\u20139 September, 2006. Lecture notes in computer science, vol 4184. Springer, Berlin, pp 273\u2013287"},{"key":"134_CR52","unstructured":"Zhu H (2005) Linking the semantics of a multithreaded discrete event simulation language. PhD thesis, London South Bank University, February 2005"},{"key":"134_CR53","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, pp 139\u2013151"},{"key":"134_CR54","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, 2007. Lecture notes in computer science, vol 4882. Springer, Berlin, pp 225\u2013239","DOI":"10.1007\/978-3-540-77115-9_23"},{"key":"134_CR55","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, pp 315\u2013326","DOI":"10.1109\/SEFM.2007.4"},{"key":"134_CR56","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, 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-010-0134-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-010-0134-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-010-0134-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T13:47:45Z","timestamp":1559396865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-010-0134-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4,30]]},"references-count":56,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["134"],"URL":"https:\/\/doi.org\/10.1007\/s11334-010-0134-z","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4,30]]}}}