{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T19:21:46Z","timestamp":1648581706928},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The current dominance of the service-based paradigm reflects the success of specific design and architectural principles embodied in terms like SOA and REST. This paper suggests further principles for the design of services exhibiting long-running transactions (that is, transactions whose characteristic feature is that in the case of failure not all system states can be automatically restored: system compensation is required). The principles are expressed at the level of scope-based compensation and fault handling, and ensure the consistency of data critical to the business logic. They do so by demanding (a) either the commitment of all of the transaction or none of it, and (b) that compensation is assured in case of failure in \u2018parent\u2019 transactions. The notion of scope is captured algebraically (rather than semantically) in order to express design guidelines which ensure that a given transaction satisfies those principles. Transactional processes are constructed by parallel composition of services, and transactions with scopes in a single service are dealt with as a special case. The system semantics is formalised as a transition system (in Z) and the principles are expressed as formulae in linear temporal logic over runs of the transition system. That facilitates the model checking (using SAL) of their bounded versions. Two simple examples are used throughout to illustrate definitions and finally to demonstrate the approach.<\/jats:p>","DOI":"10.1007\/s00165-013-0275-6","type":"journal-article","created":{"date-parts":[[2013,3,27]],"date-time":"2013-03-27T15:32:37Z","timestamp":1364398357000},"page":"623-676","source":"Crossref","is-referenced-by-count":0,"title":["Compensation by design"],"prefix":"10.1145","volume":"26","author":[{"given":"Xi","family":"Liu","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China"}]},{"given":"Shaofa","family":"Yang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}]},{"given":"J. W.","family":"Sanders","sequence":"additional","affiliation":[{"name":"African Institute for Mathematical Sciences, Muizenberg and Stellenbosch University, Stellenbosch, South Africa"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Bruni R Butler MJ Ferreira C Hoare CAR Melgratti HC Montanari U (2005) Comparing two approaches to compensable flow composition. In: Proceedings of the international conference concurrency theory (CONCUR\u201905) San Francisco CA USA 23\u201326 Aug 2005 pp 383\u2013397","DOI":"10.1007\/11539452_30"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Butler M Ferreira C (2004) An operational semantics for StAC a language for modelling long-running business transactions. In Coordination Models and Languages (COORDINATION\u201904) vol 2949 of lecture notes in computer science. Springer Berlin","DOI":"10.1007\/978-3-540-24634-3_9"},{"issue":"5","key":"e_1_2_1_2_3_2","first-page":"712","article-title":"Precise modelling of compensating business transactions and its application to BPEL","volume":"11","author":"Butler M","year":"2005","journal-title":"J Univers Comput Sci"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Butler M Hoare CAR Ferreira C (2004) A trace semantics for long-running transactions. In 25\u00a0years of communicating sequential processes Springer Berlin pp 133\u2013150","DOI":"10.1007\/11423348_8"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bhattacharya K Hull R Su J (2009) A data-centric design methodology for business processes. In: Handbook of research on business process modeling IGI Global Hershey 2009 pp 503\u2013531","DOI":"10.4018\/978-1-60566-288-6.ch023"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.09.021"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bruni R Melgratti HC Montanari U (2005) Theoretical foundations for compensations in flow composition languages. In: Proceedings of the ACM symposium on principles of programming languages (POPL\u201905) Long Beach CA USA 12\u201314 Jan 2005 pp 209\u2013220","DOI":"10.1145\/1047659.1040323"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Butler MJ Ripon S (2005) Executable semantics for compensating CSP. In: Proceedings of formal techniques for computer systems and business processes Versailles France 1\u20133 Sept 2005 pp 243\u2013256","DOI":"10.1007\/11549970_18"},{"key":"e_1_2_1_2_9_2","unstructured":"Coleman JW (2005) Examining BPEL\u2019s compensation construct. In: Proceedings of workshop on rigorous engineering of fault-tolerant systems (REFT) 2005 pp 122\u2013128"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006916"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"De Vries E Koutavas V Hennessy M (2010) Communicating transactions. In: CONCUR 2010\u2014concurrency theory vol 6269 of lecture notes in computer science Springer Berlin pp 569\u2013583","DOI":"10.1007\/978-3-642-15375-4_39"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"De Vries E Koutavas V Hennessy M (2010) Liveness of communicating transactions (extended abstract). In: Programming languages and systems vol 6461 of lecture notes in computer science Springer Berlin 2010 pp 392\u2013407","DOI":"10.1007\/978-3-642-17164-2_27"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"de Moura L Owre S Rue\u00df H Rushby J Shankar N Sorea M Tiwari A (2004) SAL 2. In: Computer aided verification (CAV\u201904) vol 3114 of lecture notes in computer science Springer Berlin\/Heidelberg pp 251\u2013254","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"e_1_2_1_2_14_2","unstructured":"de Moura L Shankar N (2003) The SAL language manual. Technical report SRI-CSL-01-02 (rev. 02) SRI International 2003"},{"key":"e_1_2_1_2_15_2","unstructured":"Fielding RT (2000) Architectural styles and the design of network-based software architectures. Ph.D. dissertation University of California Irvine"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/514183.514185"},{"key":"e_1_2_1_2_17_2","unstructured":"Greenfield P Fekete A Jang J Kuo D (2003) Compensation is not enough. In: Proceedings of the international conference on enterprise distributed object computing (EDOC\u201903) Brisbane Australia Sept 2003 pp 232\u2013239"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Garcia-Molina H Salem K (1987) Sagas. In: Proceedings of the 1987 ACM SIGMOD international conference on management of data (SIGMOD\u201987) San Francisco CA pp 249\u2013259","DOI":"10.1145\/38713.38742"},{"key":"e_1_2_1_2_19_2","unstructured":"Gray J Reuter A (1993) Transaction processing: concepts and techniques. Morgan Kaufmann Publishers San Mateo"},{"key":"e_1_2_1_2_20_2","unstructured":"He J (2007) UTP semantics for web services. In: Proceedings of the international conference on integrated formal methods (IFM\u201907) Oxford UK 2\u20135 July 2007 Springer Berlin pp 353\u2013372"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"He J (2008) Transaction calculus. In: Proceedings of the IEEE high assurance systems engineering symposium (HASE\u201908) Nanjing China p 4","DOI":"10.1109\/HASE.2008.67"},{"key":"e_1_2_1_2_22_2","unstructured":"Korth HF Levy E Silberschatz A (1990) A formal approach to recovery by compensating transactions. In: Proceedings of the international conference on very large data bases (VLDB\u201990) Brisbane Australia pp 95\u2013106"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Kopp O Mietzner R Leymann F (2009) The influence of an external transaction on a BPEL scope. In: On the move to meaningful internet systems (OTM\u201909) vol 5870 of lecture notes in computer science Springer Berlin\/Heidelberg 2009 pp 381\u2013388","DOI":"10.1007\/978-3-642-05148-7_27"},{"issue":"4","key":"e_1_2_1_2_24_2","first-page":"635","article-title":"Describing and verifying web service using pi-calculus","volume":"28","author":"Liao J","year":"2005","journal-title":"Chin J Comput"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Li J Zhu H He J (2007) Algebraic semantics for compensable transactions. In: Proceedings of the international conference on theoretical aspects of computing (ICTAC\u201907) 2007 pp 306\u2013321","DOI":"10.1007\/978-3-540-75292-9_21"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10257-005-0026-1"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Mendling J Simon C (2006) Business process design by view integration. In: Business process management workshops vol 4103 of lecture notes in computer science Springer Berlin\/Heidelberg 2006 pp 55\u201364","DOI":"10.1007\/11837862_7"},{"key":"e_1_2_1_2_28_2","unstructured":"OASIS Web Services Business Process Execution Language (WSBPEL) TC (2007) Web services business process execution language version 2.0. OASIS standard 2007"},{"key":"e_1_2_1_2_29_2","unstructured":"OASIS Web Services Transaction (WS-TX) TC (2009) Web services atomic transaction (WS-AtomicTransaction) version 1.2. 2009"},{"key":"e_1_2_1_2_30_2","unstructured":"OASIS Web Services Transaction (WS-TX) TC (2009) Web services business activity (WS-BusinessActivity) version 1.2. OASIS Standard 2009"},{"key":"e_1_2_1_2_31_2","unstructured":"OASIS Web Services Transaction (WS-TX) TC (2009) Web services coordination (WS-Coordination) version 1.2. OASIS Standard 2009"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Pottinger S Mietzner R Leymann F (2007) Coordinate BPEL scopes and processes by extending the WS-business activity framework. In: Proceedings of OTM Confederated international conference on On the move to meaningful internet systems Springer Berlin\/Heidelberg 2007 pp 336\u2013352","DOI":"10.1007\/978-3-540-76848-7_22"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of annual symposium on foundations of computer science IEEE Computer Soceity Press Los Alamitos pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Peled D Pelliccione P Spoletini P (2009) Model checking. Wiley Encyclopedia of computer science and engineering Wiley Chichester","DOI":"10.1002\/9780470050118.ecse247"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Qiu Z Wang S Pu G Zhao X (2005) Semantics of BPEL4WS-like fault and compensation handling. In: FM 2005: formal methods vol 3582 of lecture notes in computer science Springer Berlin\/Heidelberg 2005 pp 350\u2013365","DOI":"10.1007\/11526841_24"},{"key":"e_1_2_1_2_36_2","unstructured":"Ripon S Butler MJ (2010) Deriving relationships between semantic models\u2014an approach for cCSP. CoRR abs\/1002.3330 2010"},{"key":"e_1_2_1_2_37_2","unstructured":"Ripon S Butler MJ (2010) Formalizing cCSP synchronous semantics in PVS. CoRR abs\/1001.3464 2010"},{"key":"e_1_2_1_2_38_2","unstructured":"Sun C-A el Khoury E Aiello M (2010) Transaction management in service-oriented systems: requirements and a proposal. IEEE Trans Serv Comput 99 (preprints) 2010."},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Sauter P Melzer I (2005) A comparison of WS-business activity and BPEL4WS long-running transaction. In: Kommunikation in verteilten systemen (KiVS) Informatik aktuell Springer Berlin 2005 pp 115\u2013125","DOI":"10.1007\/3-540-27301-8_10"},{"key":"e_1_2_1_2_40_2","unstructured":"Spivey JM (1992) The Z notation: a reference manual. 2nd edn Prentice Hall Englewood Cliffs"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Smith G Wildman L (2005) Model checking Z specifications using SAL. In: Formal specification and development in Z and B (ZB\u201903) vol 3455 of lecture notes in computer science Springer Berlin\/Heidelberg 2005 pp 85\u2013103","DOI":"10.1007\/11415787_6"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Wang R Salzberg B Lomet D (2010) Log-based middleware server recovery with transaction support. VLDB J: 1\u201324","DOI":"10.1007\/s00778-010-0199-1"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.3923\/itj.2011.1194.1200"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-013-0275-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-013-0275-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-013-0275-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:01:59Z","timestamp":1641484919000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-013-0275-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1007\/s00165-013-0275-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-013-0275-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7]]}}}