Abstract
Web services have become more and more important in these years, and BPEL4WS (BPEL) is a de facto standard for the web service composition and orchestration. It contains several distinct features, including the scope-based compensation and fault handling mechanism. We have considered the operational semantics and denotational semantics for BPEL, where a set of algebraic laws can be achieved via these two models, respectively. In this paper, we consider the inverse work, deriving the operational semantics and denotational semantics from algebraic semantics for BPEL. In our model, we introduce four types of typical programs, by which every program can be expressed as the summation of these four types. Based on the algebraic semantics, the strategy for deriving the operational semantics is provided and a transition system is derived by strict proof. This can be considered as the soundness exploration for the operational semantics based on the algebraic semantics. Further, the equivalence between the derivation strategy and the derived transition system is explored, which can be considered as the completeness of the operational semantics. Finally, the derivation of the denotational semantics from algebraic semantics is explored, which can support to reason about more program properties easily.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Abrial J-R (1996) The B-book: assigning programs to meanings. University Press, Cambridge
Brookes SD (1996) Full abstraction for a shared-variable parallel language. Inf Comput 127(2): 145–163
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–3, 2005. Lecture notes in computer science, vol 3670. Springer, Berlin, pp 272–286
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–14, 2005. ACM, USA, pp 209–220
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–3, 2005. Lecture notes in computer science, vol 3670. Springer, Berlin, pp 243–256
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–3, 2000. Lecture notes in computer science, vol 1945. Springer, Berlin, pp 61–76
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–27, 2004. Lecture notes in computer science, vol 2949. Springer, Berlin, pp 87–104
Butler MJ, Ferreira C, Ng MY (2005) Precise modelling of compensating business transactions and its application to BPEL. J Univers Comput Sci 11(5): 712–743
Butler MJ, Hoare CAR, Ferreira C (2005) A trace semantics for long-running transactions. In: Communicating sequential processes: the first 25 years, symposium on the occasion of 25 years of CSP, London, UK, July 7–8, 2004. Lecture notes in computer science, vol 3525. Springer, Berlin, pp 133–150
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
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
Davis J (1993) Specification and proof in real-time CSP. University Press, Cambridge
de Bakker J, de Vink E (1996) Control flow semantics. MIT Press, Massachusetts
Dijkstra EW (1976) A discipline of programming. Prentice Hall International Series in Automatic Computation
Garcia-Molina H, Salem K (1987) Sagas. In: Proceedings of ACM SIGMOD international conference on management of data, San Francisco, California, USA, May 27–29, 1987. ACM, USA, pp 249–259
Glabbeek Rv (1993) The linear time—branching time spectrum II; the semantics of sequential systems with silent moves (extended abstract). In: Best E (ed) Proceedings of CONCUR’93: 4th international conference on concurrency theory, Hildesheim, Germany, August 1993. Lecture notes in computer science, vol 715. Springer, Berlin, pp 66–81
Glabbeek Rv (1996) Comparative Concurrency Semantics and Refinement of Actions. CWI Tract, vol 109. CWI, Amsterdam (Second edition of dissertation)
Glabbeek Rv (2001) The linear time—branching time spectrum I; the semantics of concrete, sequential processes. In: Bergstra J, Ponse A, Smolka S (eds) Handbook of process algebra, chapt 1. Elsevier, Amsterdam, pp 3–99
He J (2008) Modelling coordination and compensation. In: Proceedings of ISoLA 2008: 3rd international symposium on leveraging applications of formal methods, verification and validation, Porto Sani, Greece, 13–15 October. Communications in Computer and Information Science, vol 17. Springer, Berlin, pp 15–36
He J, Zhu H, Pu G (2007) A model for BPEL-like languages. Front Comput Sci China 1(1): 9–19
Hoare CAR (1978) Communicating sequential processes. Commun ACM 21(8): 666–677
Hoare CAR (1985) Communicating sequential processes. Prentice Hall International Series in Computer Science
Hoare CAR, Hayes IJ, He J, Morgan C, Roscoe AW, Sanders JW, Sørensen IH, Spivey JM, Sufrin B (1987) Laws of programming. Commun ACM 38(8): 672–686
Hoare CAR, He J (1993) From algebra to operational semantics. Inf Process Lett 45: 75–80
Hoare CAR, He J (1998) Unifying theories of programming. Prentice Hall International Series in Computer Science
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, Massachusetts
Koshkina M, van Breugel F (2004) Modelling and verifying web service orchestration by means of the concurrency workbench. ACM SIGSOFT Softw Eng Notes 29(5): 1–10
Laneve C, Zavattaro G (2005) Web-pi at work. In: Proceedings of TGC 2005: international symposium on trustworthy global computing, Edinburgh, UK, April 7–9, 2005. Lecture notes in computer science, vol 3705. Springer, Berlin, pp 182–194
Lanotte R, Maggiolo-Schettini A, Milazzo P, Troina A (2008) Design and verification of long-running transactions in a timed framework. Sci Comput Program 73(2–3): 76–94
Leymann F (2001) Web Services Flow Language (WSFL 1.0). IBM http://www-3.ibm.com/software/solutions/webservices/pdf/WSDL.pdf
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, Los Angeles, pp 154–166
Lucchi R, Mazzara M (2007) A pi-calculus based semantics for ws-bpel. J Log Algebraic Program 70(1): 96–118
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, Los Angeles, pp 151–158
Luo C, Qin S, Qiu Z (2008) Verifying bpel-like programs with hoare logic. Front Comput Sci China 2(4): 344–356
Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin
Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin
McIver A, Morgan C (2004) Abstraction, refinement and proof of probability systems. monographs in computer science. Springer, Berlin
Milner R (1999) Communication and mobile system: π-calculus. University Press, Cambridge
Moss J (1981) Nested transactions: an approach to reliable distributed computing. PhD thesis, Department of Electrical Engineering and Computer Science, MIT, April
Plotkin G (2004) A structural approach to operational semantics. Technical report 19, University of Aahus, 1981. J Log Algebraic Program 60–61:17–139
Pu G, Zhao X, Wang S, Qiu Z (2006) Towards the semantics and verification of BPEL4WS. Electron Notes Theor Comput Sci 151(2): 33–52
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–16 June, 2006. Lecture notes in computer science, vol 4307. Springer, Berlin, pp 251–266.
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–22, 2005. Lecture notes in computer science, vol 3582. Springer, Berlin, pp 350–365
Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall International Series in Computer Science
Scott D, Strachey C (1971) Towards a mathematical semantics for computer languages. Technical report PRG-6, Oxford University Computer Laboratory
Thatte S (2001) XLANG: Web Service for Business Process Design. Microsoft, http://www.gotdotnet.com/team/xml_wsspecs/xlang-c/default.html
van Breugel F, Koshkina M (2005) Dead-path-elimination in bpel4ws. In: Proceedings of ACSD 2005: fifth international conference on application of concurrency to system design, pp 192–201, St. Malo, France, June, IEEE Computer Society, Los Angeles
Zhu H (2005) Linking the semantics of a multithreaded discrete event simulation language. PhD thesis, London, South Bank University, February
Zhu H, Bowen JP, He J (2002) Soundness, completeness and non-redundancy of operational semantics for Verilog based on denotational semantics. In: Proceedings of ICFEM 2002: 4th international conference on formal engineering methods. Lecture notes in computer science, vol 2495. Springer, Berlin, pp 600–612
Zhu H, He J (2000) A semantics of Verilog using duration calculus. In: Proceedings of international conference on software: theory and practice, pp 421–432
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, Los Angeles, pp 139–151
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–20 December. Lecture notes in computer science, vol 4882. Springer, Berlin, pp 225–239
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, Los Angeles, pp 315–326
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, Los Angeles, pp 236–245
Author information
Authors and Affiliations
Corresponding author
Additional information
A short version of this paper appeared in SEFM 2007: 5th IEEE International Conference on Software Engineering and Formal Methods [53].
Rights and permissions
About this article
Cite this article
Zhu, H., He, J., Li, J. et al. Algebraic approach to linking the semantics of web services. Innovations Syst Softw Eng 7, 209–224 (2011). https://doi.org/10.1007/s11334-011-0172-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-011-0172-1