×

Failure-divergence semantics and refinement of long running transactions. (English) Zbl 1279.68202

Summary: Compensating CSP (cCSP) models long-running transactions. It can be used to specify service orchestrations written in programming languages like WS-BPEL. However, the original cCSP does not allow to model internal (non-deterministic) choice, synchronized parallel composition, hiding or recursion. In this paper, we introduce these operators and define for the extended language a failure-divergence (FD) semantics to allow reasoning about non-determinism, deadlock and livelock. Furthermore, we develop a refinement calculus that allows us to compare the level of non-determinism between long running transactions, and transform specifications for design and analysis.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

COWS; rCOS; CSP-prover
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] A. Alves, A. Arkin, S. Askary, B. Bloch, F. Curbera, Y. Goland, N. Kartha, Sterling, D. König, V. Mehta, S. Thatte, D. van der Rijn, P. Yendluri, A. Yiu, Web services business process execution language version 2.0, OASIS Committee Draft, May 2006.; A. Alves, A. Arkin, S. Askary, B. Bloch, F. Curbera, Y. Goland, N. Kartha, Sterling, D. König, V. Mehta, S. Thatte, D. van der Rijn, P. Yendluri, A. Yiu, Web services business process execution language version 2.0, OASIS Committee Draft, May 2006.
[2] Bocchi, L.; Laneve, C.; Zavattaro, G., A calculus for long-running transactions, (Najm, E.; Nestmann, U.; Stevens, P., FMOODS. FMOODS, Lecture Notes in Computer Science, vol. 2884 (2003), Springer) · Zbl 1253.68056
[3] Bravetti, M.; Zavattaro, G., On the expressive power of process interruption and compensation, Mathematical Structures in Computer Science, 19, 3, 565-599 (2009) · Zbl 1186.68317
[4] Bruni, R.; Butler, M. J.; Ferreira, C.; Hoare, C. A.R.; Melgratti, H. C.; Montanari, U., Comparing two approaches to compensable flow composition, (Abadi, M.; de Alfaro, L., CONCUR. CONCUR, Lecture Notes in Computer Science, vol. 3653 (2005), Springer) · Zbl 1134.68316
[5] Bruni, R.; Melgratti, H. C.; Montanari, U., Nested commits for mobile calculi: extending join, (Lévy, J.-J.; Mayr, E. W.; Mitchell, J. C., IFIP (2004), TCS, Kluwer) · Zbl 1088.68507
[6] Bruni, R.; Melgratti, H. C.; Montanari, U., Theoretical foundations for compensations in flow composition languages, (Palsberg, J.; Abadi, M., POPL (2005), ACM) · Zbl 1369.68070
[7] Butler, M. J.; Ferreira, C., An operational semantics for StAC, a language for modelling long-running business transactions, (Nicola, R. D.; Ferrari, G. L.; Meredith, G., COORDINATION. COORDINATION, Lecture Notes in Computer Science, vol. 2949 (2004), Springer) · Zbl 1081.68643
[8] Butler, M. J.; Ferreira, C.; Ng, M. Y., Precise modelling of compensating business transactions and its application to BPEL, Journal of Universal Computer Science, 11, 5, 712-743 (2005)
[9] Butler, M. J.; Hoare, C. A.R.; Ferreira, C., A trace semantics for long-running transactions, (Abdallah, A. E.; Jones, C. B.; Sanders, J. W., 25 Years Communicating Sequential Processes. 25 Years Communicating Sequential Processes, Lecture Notes in Computer Science, vol. 3525 (2004), Springer) · Zbl 1081.68644
[10] Butler, M. J.; Ripon, S., Executable semantics for compensating CSP, (Bravetti, M.; Kloul, L.; Zavattaro, G., EPEW/WS-FM. EPEW/WS-FM, Lecture Notes in Computer Science, vol. 3670 (2005), Springer)
[11] Castagna, G.; Gesbert, N.; Padovani, L., A theory of contracts for web services, (Necula, G. C.; Wadler, P., POPL (2008), ACM) · Zbl 1295.68080
[12] Chen, Z.; Liu, Z., An extended cCSP with stable failures semantics, (Cavalcanti, A.; Déharbe, D.; Gaudel, M.-C.; Woodcock, J., ICTAC. ICTAC, Lecture Notes in Computer Science, vol. 6255 (2010), Springer) · Zbl 1286.68312
[13] Chen, Z.; Liu, Z.; Wang, J., Failure-divergence refinement of compensating communicating processes, (Butler, M.; Schulte, W., FM. FM, Lecture Notes in Computer Science, vol. 6664 (2011), Springer)
[14] Chen, Z.; Wang, J.; Dong, W.; Qi, Z., Towards formal interfaces for web services with transactions, (Damiani, E.; Yétongnon, K.; Chbeir, R.; Dipanda, A., SITIS. SITIS, Lecture Notes in Computer Science, vol. 4879 (2006), Springer)
[15] Garcia-Molina, H.; Salem, K., (Dayal, U.; Traiger, I. L., SIGMOD Conference (1987), ACM Press)
[16] Guidi, C.; Lucchi, R.; Gorrieri, R.; Busi, N.; Zavattaro, G., SOCK: A calculus for service oriented computing, (Dan, A.; Lamersdorf, W., ICSOC. ICSOC, Lecture Notes in Computer Science, vol. 4294 (2006), Springer)
[17] He, J., UTP semantics for web services, (Davies, J.; Gibbons, J., IFM. IFM, Lecture Notes in Computer Science, vol. 4591 (2007), Springer) · Zbl 1213.68111
[18] Hoare, C.; Jifeng, H., Unifying Theories of Programming (1998), Prentice Hall
[19] Isobe, Y.; Roggenbach, M., A generic theorem prover of CSP refinement, (Halbwachs, N.; Zuck, L. D., TACAS. TACAS, Lecture Notes in Computer Science, vol. 3440 (2005), Springer) · Zbl 1087.68592
[20] Lanese, I.; Vaz, C.; Ferreira, C., On the expressive power of primitives for compensation handling, (Gordon, A. D., ESOP. ESOP, Lecture Notes in Computer Science, vol. 6012 (2010), Springer) · Zbl 1260.68102
[21] Lanese, I.; Zavattaro, G., Programming sagas in SOCK, (Hung, D. V.; Krishnan, P., SEFM (2009), IEEE Computer Society)
[22] Laneve, C.; Zavattaro, G., Foundations of web transactions, (Sassone, V., FoSSaCS. FoSSaCS, Lecture Notes in Computer Science, vol. 3441 (2005), Springer) · Zbl 1118.68335
[23] Lanotte, R.; Maggiolo-Schettini, A.; Milazzo, P.; Troina, A., Modeling long-running transactions with communicating hierarchical timed automata, (Gorrieri, R.; Wehrheim, H., FMOODS. FMOODS, Lecture Notes in Computer Science, vol. 4037 (2006), Springer) · Zbl 1461.68136
[24] Lapadula, A.; Pugliese, R.; Tiezzi, F., A calculus for orchestration of web services, (Nicola, R. D., ESOP. ESOP, Lecture Notes in Computer Science, vol. 4421 (2007), Springer) · Zbl 1187.68070
[25] Little, M. C., Transactions and web services, Communications of the ACM, 46, 10, 49-54 (2003)
[26] Liu, Z.; Joseph, M., Transformation of programs for fault-tolerance, Formal Aspects of Computing, 4, 5, 442-469 (1992) · Zbl 0754.68084
[27] Liu, Z.; Joseph, M., Specification and verification of recovery in asynchronous communicating systems, (Vytopil, J., Formal techniques in real-time and fault-tolerant systems (1993), Kluwer Academic Publishers), 137-165
[28] Liu, Z.; Joseph, M., Specification and verification of fault-tolerance, timing, and scheduling, ACM Transactions on Programming Languages and Systems, 21, 1, 46-89 (1999)
[29] Liu, Z.; Morisset, C.; Stolz, V., rCOS: Theory and tool for component-based model driven development, (Arbab, F.; Sirjani, M., FSEN. FSEN, Lecture Notes in Computer Science, vol. 5961 (2009), Springer)
[30] Mazzara, M.; Lanese, I., Towards a unifying theory for web services composition, (Bravetti, M.; Núñez, M.; Zavattaro, G., WS-FM. WS-FM, Lecture Notes in Computer Science, vol. 4184 (2006), Springer)
[31] Milner, R., A Calculus of Communicating Systems (1982), Springer-Verlag New York, Inc: Springer-Verlag New York, Inc Secaucus, NJ, USA
[32] S. Ripon, Extending and relating semantic models of compensating CSP, Ph.D. thesis, University of Southampton, 2008.; S. Ripon, Extending and relating semantic models of compensating CSP, Ph.D. thesis, University of Southampton, 2008.
[33] Ripon, S.; Butler, M. J., PVS embedding of cCSP semantic models and their relationship, Electronic Notes in Theoretical Computer Science, 250, 2, 103-118 (2009) · Zbl 1335.68129
[34] Roscoe, A. W., The Theory and Practice of Concurrency (1997), Prentice Hall PTR: Prentice Hall PTR Upper Saddle River, NJ, USA
[35] Roscoe, A. W., The three platonic models of divergence-strict CSP, (Proc. ICTAC. Proc. ICTAC, Lecture Notes in Computer Science, vol. 5160 (2008)) · Zbl 1161.68629
[36] Sun, J.; Liu, Y.; Dong, J. S., Model checking CSP revisited: introducing a process analysis toolkit, (Margaria, T.; Steffen, B., ISoLA. ISoLA, Communications in Computer and Information Science, vol. 17 (2008), Springer)
[37] S. Thatte, XLANG Web Services for Business Process Design, 2001.; S. Thatte, XLANG Web Services for Business Process Design, 2001.
[38] Vaz, C.; Ferreira, C.; Ravara, A., Dynamic recovering of long running transactions, (Kaklamanis, C.; Nielson, F., TGC. TGC, Lecture Notes in Computer Science, vol. 5474 (2008), Springer)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.