Abstract
We study the foundations of Web service technologies for connecting abstract and concrete service definitions and for discovering services according to their observable behavior. We pursue this study addressing a subset of BPEL activities that include concurrency constructs. We present a formal semantics—called compliance preorder—of this subset of BPEL and we define a behavioral type discipline that guarantees the correctness of client-server interactions. The types of our discipline, called contracts, are De Nicola and Hennessy tau-less, finite-state CCS processes. We show that contracts are BPEL normal forms according to the compliance preorder and that the compliance preorder does coincide with a well-known equivalence in concurrency theory, the must-testing preorder. The compliace preorder is not fully adequate for discovering Web services though, since it does not support width and depth extensions of Web services. To address this issue, we propose a sound generalization of the compliance preorder, called subcontract relation, that admits a notion of principal service contract—the dual contract—compliant with a given client contract and that exhibits good precongruence properties when choreographies of Web services are considered.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abramsky S (1990) The lazy lambda calculus. In: Proceedings of research topics in functional programming, Addison-Wesley, Boston, MA, pp 65–116
Aceto L, Ingolfsdottir A, Srba J (2011) The algoritmics of bisimilarity. In: Sangiorgi D, Rutten J (eds) Advanced topics in bisimulation and coinduction of Cambridge tracts in theoretical computer science, chapter 3, vol 52. Cambridge University Press, pp 100–172
Alves A et al. (2007) Web Services Business Process Execution Language Version 2.0. http://docs.oasis-open.org/wsbpel/2.0/CS01/wsbpel-v2.0-CS01.html
Banerji A, Bartolini C, Beringer D, Chopella V et al. (2002) Web Services Conversation Language (WSCL) 1.0. http://www.w3.org/TR/2002/NOTE-wscl10-20020314
Barbanera F, Capecchi S, de’Liguoro U (2009) Typing asymmetric client-server interaction. In: Proceedings of fundamentals of software engineering, third IPM international conference, FSEN 2009, Kish Island, Iran, April 15–17, 2009, revised selected papers, of Lecture Notes in Computer Science, vol 5961. Springer, pp 97–112
Benzaken V, Castagna G, Frisch A (2003) CDuce: an XML-centric general-purpose language. SIGPLAN Not 38(9): 51–63
Bernardi G (2013) Behavioural Equivalences for Web Services. PhD thesis, University of Dublin
Busi N, Gabbrielli M, Zavattaro G (2009) On the expressive power of recursion, replication and iteration in process calculi. Math Struct Comput Sci 19(6): 1191–1222
Bernardi G, Hennessy M (2012) Modelling session types using contracts. In: Proceedings of the 27th annual ACM symposium on applied computing, SAC ’12, ACM, New York, pp 1941–1946
Brookes SD, Hoare CAR, Roscoe AW (1984) A theory of communicating sequential processes. J ACM 31(3): 560–599
Beringer D, Kuno H, Lemon M (2001) Using WSCL in a UDDI Registry 1.0, UDDI Working draft best practices document. http://xml.coverpages.org/HP-UDDI-wscl-5-16-01.pdf
Bravetti M, Lanese I, Zavattaro G (2009) Contract-driven implementation of choreographies. In: Proceedings of trustworthy global computing, lecture notes in computer science, vol. 5474. Springer, pp 1–18
Bugliesi M, Macedonio D, Pino L, Rossi S (2009) Compliance preorders for web services. In: Proceedings of WS-FM, lecture notes in computer science, vol. 6194. Springer, pp 76–91
Boreale M, Sangiorgi D (1998) Bisimulation in name-passing calculi without matching. In: Proceedings of logic in computer science, 1998. thirteenth annual IEEE Symposium, pp 165–175
Bravetti M, Zavattaro G (2007) Towards a unifying theory for choreography conformance and contract compliance. In Proceedings of SC 2007, LNCS, vol 4829. Springer, pp 34–50
Bravetti M, Zavattaro G (2008) A foundational theory of contracts for multi-party service composition. Fundam Inform 89(4): 451–478
Bravetti M, Zavattaro G (2009) Contract-based discovery and composition of web services. In: Proceedings of SFM’09, lecture notes in computer science, vol 5569. Springer, pp 261–295
Bravetti M, Zavattaro G (2009) A theory of contracts for strong service compliance. Math Struct Comput Sci 19: 601–638
Carpineti S, Castagna G, Laneve C, Padovani L (2006) A formal account of contracts for web services. In: Proceedings of WS-FM, 3rd international workshop on web services and formal methods, in LNCS, vol 4184. Springer, pp 148–162
Christensen E, Curbera F, Meredith G, Weerawarana S (2001) Web services description language (WSDL) 1.1. http://www.w3.org/TR/2001/NOTE-wsdl-20010315
Castagna G, Gesbert N, Padovani L (2009) A theory of contracts for web services. ACM Trans Program Lang Syst 31(5): 19
Carbone M, Honda K, Yoshida N (2007) Structured communication-centered programming for web services. In: Proceedings of 16th European symposium on programming, (ESOP’07), LNCS 4421. Springer, pp 2–17
Carpineti S, Laneve C, Padovani L (2009) PiDuce: A project for experimenting web services technologies. Sci Comput Program 74(10): 777–811
Di Cosmo R (1995) Isomorphisms of types: from Lambda calculus to information retrieval and language desig. Birkhauser, Basel. ISBN-0-8176-3763-X
Castagna G, Padovani L (2009) Contracts for mobile processes. In: Proceedings of the 20th international conference on concurrency theory (CONCUR’09), of LNCS, vol 5710. Springer, pp 211–228
Cleaveland R, Parrow J, Steffen B (1993) The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans Program Lang Syst 15(1): 36–72
Chaki S, Rajamani SK, Rehof J (2002) Types as models: model checking message-passing programs. SIGPLAN Not 37(1): 45–57
De Nicola R, Hennessy M (1984) Testing equivalences for processes. Theor Comput Sci 34: 83–133
De Nicola R, Hennessy M (1987) CCS without τ’s. In: Proceedings of TAPSOFT’87/CAAP’87, LNCS 249. Springer, pp 138–152
Fournet C, Laneve C (2001) Bisimulations in the join-calculus. Theor Comput Sci 266(1–2): 569–603
Gay S, Hole M (2005) Subtyping for session types in the π-calculus. Acta Informatica 42(2–3): 191–225
Hennessy M (1988) Algebraic theory of processes: foundation of computing. MIT Press
Honda K (1993) Types for dyadic interaction. In: Proceedings of CONCUR’93, LNCS 715. Springer, pp 509–523
Hosoya H, Pierce BC (2003) XDuce: a statically typed XML processing language. ACM Trans Internet Tech 3(2): 117–148
Honda K, Vasconcelos VT, Kubo M (1998) Language primitives and type disciplines for structured communication-based programming. In: Proceedings of ESOP’98, LNCS 1381. Springer, New York, pp 122–138
Honda K, Yoshida N, Carbone M (2008) Multiparty asynchronous session types. In: Proceedings of POPL 2008. ACM, pp 273–284
Igarashi A, Kobayashi N (2001) A generic type system for the pi-calculus. In: Proceedings of POPL 2001, ACM, pp 128–141
Kavantzas N, Burdett D, Ritzinger G, Fletcher T, Lafon Y, Barreto C (2005) Web services choreography description language 1.0. http://www.w3.org/TR/2005/CR-ws-cdl-10-20051109/
Laneve C, Padovani L (2007) The must preorder revisited: an algebraic theory for web services contracts. In: Proceedings of CONCUR’07, LNCS 4703. Springer, pp 212–225
Laneve C, Padovani L (2008) The pairing of contracts and session types. In: Proceedings of concurrency, graphs and models, lecture notes in computer science, vol. 5065. Springer, New York, pp 681–700
Laneve C, Padovani L (2013) An algebraic theory for web service contracts. In: Proceedings of 10th international conference on integrated formal methods, LNCS, vol. 7940. Springer, New York, pp 301–315
Milner R (1982) A calculus of communicating systems. Springer
Milner R (1989) Communication and concurrency. Prentice Hall, Upper Saddle River, NJ
Nielson HR, Nielson F (1994) Higher-order concurrent programs with finite communication topology (extended abstract). In: Proceedings of POPL’94. ACM Press, New York, pp 84–97
Ouyang C, Verbeek E, van der Aalst WMP, Breutel S, Dumas M, ter Hofstede AHM (2007) Formal semantics and analysis of control flow in ws-bpel. Sci Comput Program 67(2–3):162–198
Padovani L (2008) Contract-directed synthesis of simple orchestrators. In: Proceedings of the 19th international conference on concurrency theory (CONCUR’08), LNCS, vol 5201. Springer, New York, pp 131–146
Padovani L (2009) Contract-based discovery and adaptation of web services, LNCS, vol 5569. Springer, New York, pp 213–260
Padovani L (2010) Contract-based discovery of web services modulo simple orchestrators. Theor Comput Sci 411: 3328–3347
Padovani L (2013) Fair subtyping for open session types. In: Proceedings of 40th international colloquium on automata, languages, and programming, part II, LNCS, vol 7966. Springer, New York, pp 373–384
Padovani L (2014) Fair subtyping for multi-party session types. Math Struct Comput Sci, pp 1–41
Pitts AM, Stark IDB (1993) Observable properties of higher order functions that dynamically create local names, or what’s new? In: Proceedings of 18th international symposium on mathematical foundations of computer science, lecture notes in computer science, vol 711. Springer, New York, pp 122–141
Rittri M (1993) Retrieving library functions by unifying types modulo linear isomorphism. In: Proceedings of RAIRO theoretical informatics and applications 27(6): 523–540
Author information
Authors and Affiliations
Corresponding author
Additional information
Einar Broch Johnsen, Luigia Petre, and Michael Butler
The research reported in this paper was partially funded by the EU FP7 610582 project called ENVISAGE.
Rights and permissions
About this article
Cite this article
Laneve, C., Padovani, L. An algebraic theory for web service contracts. Form Asp Comp 27, 613–640 (2015). https://doi.org/10.1007/s00165-015-0334-2
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-015-0334-2