{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T12:15:20Z","timestamp":1725624920198},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642338250"},{"type":"electronic","value":"9783642338267"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33826-7_12","type":"book-chapter","created":{"date-parts":[[2012,9,25]],"date-time":"2012-09-25T22:46:25Z","timestamp":1348613185000},"page":"172-187","source":"Crossref","is-referenced-by-count":1,"title":["The Rely\/Guarantee Approach to Verifying Concurrent BPEL Programs"],"prefix":"10.1007","author":[{"given":"Huibiao","family":"Zhu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiwen","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chris","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengchao","family":"Qin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zongyan","family":"Qiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"12_CR1","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1145\/357103.357110","volume":"2","author":"K.R. Apt","year":"1980","unstructured":"Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst.\u00a02(3), 359\u2013385 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11549970_20","volume-title":"Formal Techniques for Computer Systems and Business Processes","author":"R. Bruni","year":"2005","unstructured":"Bruni, R., Ferrari, G.L., Melgratti, H.C., Montanari, U., Strollo, D., Tuosto, E.: From Theory to Practice in Transactional Composition of Web Services. In: Bravetti, M., Kloul, L., Zavattaro, G. (eds.) EPEW\/WS-EM 2005. LNCS, vol.\u00a03670, pp. 272\u2013286. Springer, Heidelberg (2005)"},{"key":"12_CR3","first-page":"209","volume-title":"Proc. POPL 2005","author":"R. Bruni","year":"2005","unstructured":"Bruni, R., Melgratti, H.C., Montanari, U.: Theoretical foundations for compensations in flow composition languages. In: Proc. POPL 2005, January 12-14, pp. 209\u2013220. ACM, Long Beach (2005)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-24634-3_9","volume-title":"Coordination Models and Languages","author":"M.J. Butler","year":"2004","unstructured":"Butler, M.J., Ferreira, C.: An Operational Semantics for StAC, a Language for Modelling Long-Running Business Transactions. In: De Nicola, R., Ferrari, G.-L., Meredith, G. (eds.) COORDINATION 2004. LNCS, vol.\u00a02949, pp. 87\u2013104. Springer, Heidelberg (2004)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-40911-4_5","volume-title":"Integrated Formal Methods","author":"M.J. Butler","year":"2000","unstructured":"Butler, M.J., Ferreira, C.: A Process Compensation Language. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol.\u00a01945, pp. 61\u201376. Springer, Heidelberg (2000)"},{"issue":"5","key":"12_CR6","first-page":"712","volume":"11","author":"M.J. Butler","year":"2005","unstructured":"Butler, M.J., Ferreira, C., Ng, M.Y.: Precise modelling of compensating business transactions and its application to BPEL. Journal of Universal Computer Science\u00a011(5), 712\u2013743 (2005)","journal-title":"Journal of Universal Computer Science"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/11423348_8","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"M.J. Butler","year":"2005","unstructured":"Butler, M.J., Hoare, C.A.R., Ferreira, C.: A Trace Semantics for Long-Running Transactions. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) CSP25. LNCS, vol.\u00a03525, pp. 133\u2013150. Springer, Heidelberg (2005)"},{"key":"12_CR8","unstructured":"Curbera, F., Goland, Y., Klein, J., Leymann, F., Roller, D., Thatte, S., Weerawarana, S.: Business Process Execution Language for Web Service (2003)"},{"key":"12_CR9","unstructured":"de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Zwiers, M.P.J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press (2001)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Garcia-Molina, H., Salem, K.: Sagas. In: Proc. ACM SIGMOD International Conference on Management of Data, San Francisco, California, USA, May 27-29, pp. 249\u2013259. ACM (1987)","DOI":"10.1145\/38714.38742"},{"issue":"1","key":"12_CR11","doi-asserted-by":"publisher","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\u00a01(1), 9\u201319 (2007)","journal-title":"Frontiers of Computer Science in China"},{"issue":"4","key":"12_CR12","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst.\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11580850_11","volume-title":"Trustworthy Global Computing","author":"C. Laneve","year":"2005","unstructured":"Laneve, C., Zavattaro, G.: Web-Pi at Work. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol.\u00a03705, pp. 182\u2013194. Springer, Heidelberg (2005)"},{"issue":"2-3","key":"12_CR14","doi-asserted-by":"publisher","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.: Design and verification of long-running transactions in a timed framework. Science of Computer Programming\u00a073(2-3), 76\u201394 (2008)","journal-title":"Science of Computer Programming"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Leymann, F.: Web Services Flow Language (WSFL 1.0). IBM (2001)","DOI":"10.1007\/3-540-45752-6_1"},{"key":"12_CR16","first-page":"151","volume-title":"Proc. TASE 2008","author":"C. Luo","year":"2008","unstructured":"Luo, C., Qin, S., Qiu, Z.: Verifying BPEL-like programs with hoare logic. In: Proc. TASE 2008, pp. 151\u2013158. IEEE Computer Society, Nanjing (2008)"},{"key":"12_CR17","unstructured":"Moss, J.: Nested Transactions: An Approach to Reliable Distributed Computing. PhD thesis, Department of Electrical Engineering and Computer Science. MIT (April 1981)"},{"key":"12_CR18","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica\u00a06, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/11526841_24","volume-title":"FM 2005: Formal Methods","author":"Z. Qiu","year":"2005","unstructured":"Qiu, Z., Wang, S.-L., Pu, G., Zhao, X.: Semantics of BPEL4WS-Like Fault and Compensation Handling. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 350\u2013365. Springer, Heidelberg (2005)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/3-540-54430-5_110","volume-title":"CONCUR \u201991","author":"K. St\u00f8len","year":"1991","unstructured":"St\u00f8len, K.: A Method for the Development of Totally Correct Shared-State Parallel Programs. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol.\u00a0527, pp. 510\u2013525. Springer, Heidelberg (1991)"},{"key":"12_CR21","unstructured":"Thatte, S.: XLANG: Web Service for Business Process Design. Microsoft (2001)"},{"issue":"2","key":"12_CR22","doi-asserted-by":"publisher","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\u00a09(2), 149\u2013174 (1997)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33826-7_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:22:09Z","timestamp":1620130929000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33826-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642338250","9783642338267"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33826-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}