{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:11:19Z","timestamp":1761621079869,"version":"3.38.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/2.0"},{"start":{"date-parts":[[2011,11,16]],"date-time":"2011-11-16T00:00:00Z","timestamp":1321401600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/2.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A service is a remote computational facility which is made available for general use by means of a wide-area network. Several types of service arise in practice: stateless services, shared state services and services with states which are customised for individual users. A service-based orchestration is a multi-threaded computation which invokes remote services in order to deliver results back to a user (publication). In this paper a means of specifying services and reasoning about the correctness of orchestrations over<jats:italic>stateless<\/jats:italic>services is presented. As web services are potentially unreliable the termination of even finite orchestrations cannot be guaranteed. For this reason a partial-correctness powerdomain approach is proposed to capture the semantics of recursive orchestrations.<\/jats:p>","DOI":"10.1007\/s00165-011-0212-5","type":"journal-article","created":{"date-parts":[[2011,11,16]],"date-time":"2011-11-16T11:59:56Z","timestamp":1321444796000},"page":"833-846","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Reasoning about orchestrations of web services using partial correctness"],"prefix":"10.1145","volume":"25","author":[{"given":"Alan","family":"Stewart","sequence":"first","affiliation":[{"name":"School of EEE &amp; Computer Science, The Queen\u2019s University of Belfast, BT7 1NN, Belfast, Northern Ireland, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joaquim","family":"Gabarro","sequence":"additional","affiliation":[{"name":"Dep. LSI, Universitat Polit\u00e8cnica de Catalunya, Jordi Girona, 1-3, 08034, Barcelona, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anthony","family":"Keenan","sequence":"additional","affiliation":[{"name":"School of EEE &amp; Computer Science, The Queen\u2019s University of Belfast, BT7 1NN, Belfast, Northern Ireland, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0070-y"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1049\/iet-sen:20070027"},{"volume-title":"A discipline of programming","year":"1976","author":"Dijkstra EW","key":"e_1_2_1_2_4_2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Dong JS Liu Y Sun J Zhang X (2006) Verification of computation orchestration via timed automata. In: Liu Z He J (eds) Formal methods and software engineering. LNCS vol 4260 pp 226\u2013245","DOI":"10.1007\/11901433_13"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Gunter CA Scott DS (1990) Semantic domains In: van Leeuvan J (ed) Handbook of theoretical computer science: formal models and semantics. Elsevier. pp 633\u2013674","DOI":"10.1016\/B978-0-444-88074-1.50017-2"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/69610.357988"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/69610.357990"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_10_2","unstructured":"Hoare CAR (1985) Programs are predicates. In: Hoare CAR Shepherdson JC (eds) Mathematical logic and programming languages. Prentice-Hall pp 141\u2013155"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR He J (1998) Unifying theories of programming. Prentice Hall","DOI":"10.1007\/BFb0002714"},{"volume-title":"Proc of the NATO Advanced Study Institute, Engineering Theories of Software Intensive Systems","year":"2004","author":"Hoare CAR","key":"e_1_2_1_2_13_2"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Kitchin D Cook WR Misra J (2006) A language for task orchestration and its semantic properties. In: Baier C Hermanns H (eds) Proc of the international conference on concurrency theory (CONCUR). LNCS vol 4137 pp 477\u2013491","DOI":"10.1007\/11817949_32"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Kitchin D Quark A Cook W Misra J (2009) The Orc programming language. Proceedings of FMOODS\/FORTE. LNCS vol 5522 pp 1\u201325. Springer","DOI":"10.1007\/978-3-642-02138-1_1"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Kitchin D Powell E Misra J (2008) Simulation using orchestration. In: Meseguer J Rou G (eds) Proceedings of the 12th international conference on algebraic methodology and software technology 2008. LNCS vol 5140 pp 2\u201315","DOI":"10.1007\/978-3-540-79980-1_2"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Li Q Zhu H He J (2010) A denotational semantical model for Orc language. In: Cavalcanti A Deharbe D Gaudel M-C Woodcock J (eds) Theoretical aspects of computing. ICTAC 2010. LNCS vol 6255 pp 106\u2013120","DOI":"10.1007\/978-3-642-14808-8_8"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Njima NM Sanders JW (2010) Specification-oriented orchestration. In: Proceedings of the 2010 international conference on communications and mobile computing vol 01. IEEE pp 550\u2013554","DOI":"10.1109\/CMC.2010.326"},{"volume-title":"Proceedings of the NATO Advanced Study Institute, Engineering Theories of Software Intensive Systems","year":"2004","author":"Misra J","key":"e_1_2_1_2_19_2"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-006-0012-1"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Stewart A Gabarr\u00f3 J Clint M Harmer T Kilpatrick P Perrott R (2006) Managing grid computations: an Orc-based approach. In: Guo M et\u00a0al (eds) Parallel and distributed processing and applications (ISPA 2006). LNCS vol 4330 pp 278\u2013291","DOI":"10.1007\/11946441_29"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Vardoulakis D Wand M (2008) A compositional trace semantics for Orc. In: Coordination models and languages. LNCS vol 5052. Springer pp 331\u2013346","DOI":"10.1007\/978-3-540-68265-3_21"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.04.037"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0212-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-011-0212-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0212-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0212-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,14]],"date-time":"2025-03-14T03:21:16Z","timestamp":1741922476000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0212-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":24,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1007\/s00165-011-0212-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0212-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2013,11]]},"assertion":[{"value":"20 November 2009","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 August 2011","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 October 2011","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 November 2011","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}