Giuseppe Castagna
Nils Gesbert
Abstract
Contracts are behavioral descriptions of Web services. We devise a theory of contracts that formalizes the compatibility of a client with a service, and the safe replacement of a service with another service. The use of contracts statically ensures the successful completion of every possible interaction between compatible clients and services.
The technical device that underlies the theory is the filter, which is an explicit coercion preventing some possible behaviors of services and, in doing so, make services compatible with different usage scenarios. We show that filters can be seen as proofs of a sound and complete subcontracting deduction system which simultaneously refines and extends Hennessy's classical axiomatization of the must testing preorder. The relation is decidable, and the decision algorithm is obtained via a cut-elimination process that proves the coherence of subcontracting as a logical system.
Despite the richness of the technical development, the resulting approach is based on simple ideas and basic intuitions. Remarkably, its application is mostly independent of the language used to program the services or the clients. We outline the practical aspects of our theory by studying two different concrete syntaxes for contracts and applying each of them to Web services languages. We also explore implementation issues of filters and discuss the perspectives of future research this work opens.
- ]]Alves, A., Arkin, A., Askary, S., Barreto, C., et al. 2007. Web Services Business Process Execution Language Version 2.0. OASIS Standard, http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html.Google Scholar
- ]]Baeten, J. C. M., Corradini, F., and Grabmayer, C. A. 2007. A characterization of regular expressions under bisimulation. J. ACM 54, 2, 6. Google ScholarDigital Library
- ]]Banerji, A., Bartolini, C., Beringer, D., Chopella, V., et al. 2002. Web services conversation language (wscl) 1.0. W3C Note, http://www.w3.org/TR/2002/NOTE-wscl10-20020314.Google Scholar
- ]]Bellwood, T., Capell, S., Clement, L., Colgrave, J., et al. 2005. UDDI Version 3.0.2. OASIS Standard, http://uddi.org/pubs/uddi-v3.0.2-20041019.htm.Google Scholar
- ]]Berardi, D., Calvanese, D., De Giacomo, G., Lenzerini, M., and Mecella, M. 2003. Automatic composition of e-services that export their behavior. In Proceedings of the 1st International Conference on Service Oriented Computing (ICSOC), Lecture Notes in Computer Science, vol. 2910, Springer, 43--58.Google Scholar
- ]]Bernardi, G., Bugliesi, M., Macedonio, D., and Rossi, S. 2008. A theory of adaptable contract-based service composition. In Proceedings of Workshop on Global Computing Models and Technologies (GlobalComp'08). IEEE Computer Society Press.Google Scholar
- ]]Bravetti, M. and Zavattaro, G. 2007. Towards a unifying theory for choreography conformance and contract compliance. In Proceedings of the 6th International Symposium on Software Composition. Springer. Google ScholarDigital Library
- ]]Brinksma, E., Scollo, G., and Steenbergen, C. 1995. Lotos specifications, their implementations and their tests. In Conformance Testing Methodologies and Architectures for OSI Protocols. IEEE Computer Society Press, 468--479. Google ScholarDigital Library
- ]]Bruce, K. and Longo, G. 1990. A modest model of records, inheritance and bounded quantification. Inform. Comput. 87, 1/2, 196--240. Google ScholarDigital Library
- ]]Carbone, M., Honda, K., and Yoshida, N. 2007a. A calculus of global interaction based on session types. Electron. Notes Theor. Comput. Sci. 171, 3, 127--151. Google ScholarDigital Library
- ]]Carbone, M., Honda, K., and Yoshida, N. 2007b. Structured communication-centred programming for Web services. In Proceedings of the 16th European Symposium on Programming (ESOP'07). Lecture Notes in Computer Science, vol. 4421. Springer. Google ScholarDigital Library
- ]]Cardelli, L. 1988. A semantics of multiple inheritance. Inform. Comput. 76, 138--164. Google ScholarDigital Library
- ]]Carpineti, S., Castagna, G., Laneve, C., and Padovani, L. 2006. A formal account of contracts for Web Services. In Proceedings of the 3rd International Workshop on Web Services and Formal Methods. Lecture Notes in Computer Science, vol. 4184. Springer. Google ScholarDigital Library
- ]]Castagna, G., Dezani-Ciancaglini, M., Giachino, E., and Padovani, L. 2008. General session types. Tech. rep. id.: hal-00334435, CNRS - PPS, University Paris 7. http://hal.archives-ouvertes.fr/hal-00334435.Google Scholar
- ]]Castagna, G. and Frisch, A. 2005. A gentle introduction to semantic subtyping. In Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (Summary in ICALP'05). (PPDP'05). Lecture Notes in Computer Science, vol. 3580, Springer, 30--34. Google ScholarDigital Library
- ]]Castagna, G., Gesbert, N., and Padovani, L. 2007. A theory of contracts for Web services. In Proceedings of the 5th ACM-SIGPLAN Workshop on Programming Language Technologies for XML (PLAN-X'07). Google ScholarDigital Library
- ]]Castagna, G., Gesbert, N., and Padovani, L. 2008. A theory of contracts for Web services. In Proceedings of the 35th ACM Symposium on Principles of Programming Languages (POPL'08). 261--272. Google ScholarDigital Library
- ]]Chen, G. 2004. Soundness of coercion in the calculus of constructions. J. Logic Comput. 14, 3, 405--427. Google ScholarDigital Library
- ]]Chinnici, R., Haas, H., Lewis, A.-A., Moreau, J.-J., Orchard, D., and Weerawarana, S. 2007a. Web services description language (wsdl) version 2.0 Part 2: Adjuncts. W3C Recommendation, http://www.w3.org/TR/wsdl20-adjuncts/.Google Scholar
- ]]Chinnici, R., Moreau, J.-J., Ryman, A., and Weerawarana, S. 2007b. Web services description language (wsdl) version 2.0 Part 1: Core language. W3C Recommendation, http://www.w3.org/TR/wsdl20/.Google Scholar
- ]]Courcelle, B. 1983. Fundamental properties of infinite trees. Theor. Comput. Sci. 25, 95--169.Google ScholarCross Ref
- ]]De Giacomo, G. and Sardiña, S. 2007. Automatic synthesis of new behaviors from a library of available behaviors. In Proceedings of the International Joint Conference on Artificial Intelligence. 1866--1871. Google ScholarDigital Library
- ]]De Nicola, R. and Hennessy, M. 1984. Testing equivalences for processes. Theor. Comput. Sci. 34, 83--133.Google ScholarCross Ref
- ]]De Nicola, R. and Hennessy, M. 1987. CCS without τ's. In Procedings of the Colloquium on Trees and Algebra in Programming (TAPSOFT/CAAP'87). Lecture Notes in Computer Science, vol. 249. Springer, 138--152. Google ScholarDigital Library
- ]]De Nicola, R. and Labella, A. 2003. Nondeterministic regular expressions as solutions of equational systems. Theor. Comput. Sci. 302, 1--3, 179--189. Google ScholarDigital Library
- ]]Derrick, J., Bowman, H., Boiten, E., and Steen, M. 1996. Comparing LOTOS and Z refinement relations. In Proceedings of the Joint International Conference on Formal Description Techniques and Protocol Specification Testing and Verification (FORTE/PSTV'96). Chapman & Hall, 501--516. Google ScholarDigital Library
- ]]Di Cosmo, R. 1995. Isomorphisms of Types: From Lambda Calculus to Information Retrieval and Language Design. Birkhäuser. Google ScholarDigital Library
- ]]Fallside, D. C. and Walmsley, P. 2004. XML Schema part 0: Primer second edition. W3C Recommendation, http://www.w3.org/TR/xmlschema-0/.Google Scholar
- ]]Fournet, C. and Gonthier, G. 1996. The reflexive chemical abstract machine and the join-calculus. In Proceedings of the 23rd ACM Symposium on Principles of Programming Languages. ACM, 372--385. Google ScholarDigital Library
- ]]Fournet, C., Gonthier, G., Lévy, J.-J., Maranget, L., and Rémy, D. 1996. A calculus of mobile agents. In Proceedings of the International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 1119. Springer, 406--421. Google ScholarDigital Library
- ]]Fournet, C., Hoare, C. A. R., Rajamani, S. K., and Rehof, J. 2004. Stuck-free conformance. In Proceedings of the International Conference on Computer-aided Verification (CAV'04). Lecture Notes in Computer Science, vol. 3114. Springer.Google Scholar
- ]]Frisch, A., Castagna, G., and Benzaken, V. 2008. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. J. ACM 55, 4, 1--64. Google ScholarDigital Library
- ]]Gay, S. and Hole, M. 2005. Subtyping for session types in the π-calculus. Acta Informatica 42, 2--3, 191--225.Google ScholarCross Ref
- ]]Hennessy, M. 1985. Acceptance trees. J. ACM 32, 4, 896--928. Google ScholarDigital Library
- ]]Hennessy, M. 1988. Algebraic Theory of Processes. Foundation of Computing. MIT Press. Google ScholarDigital Library
- ]]Honda, K. 1993. Types for dyadic interaction. In Proceedings of the International Conference on Concurrency Theory (CONCUR'93). Lecture Notes in Computer Science, vol. 715. Springer, 509--523. Google ScholarDigital Library
- ]]Honda, K., Vasconcelos, V. T., and Kubo, M. 1998. Language primitives and type discipline for structured communication-based programming. In Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 1381. Springer. Google ScholarDigital Library
- ]]Hull, R., Benedikt, M., Christophides, V., and Su, J. 2003. E-services: A look behind the curtain. In Proceedings of the 22nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS'03). ACM, New York, 1--14. Google ScholarDigital Library
- ]]Laneve, C. and Padovani, L. 2006. Smooth orchestrators. In Proceedings of the Internatiomal Conference on Foundations of Software Science and Computation Structures, L. Aceto and A. Ingólfsdóttir, Eds. Lecture Notes in Computer Science, vol. 3921. Springer, 32--46. Google ScholarDigital Library
- ]]Laneve, C. and Padovani, L. 2007. The must preorder revisited: An algebraic theory for Web services contracts. In Proceedings of the 18th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 4703, Springer. Google ScholarDigital Library
- ]]Laneve, C. and Padovani, L. 2008. The pairing of contracts and session types. In Proceedings of the Colloquium in Honour of Ugo Montinari. Lecture Notes in Computer Science, vol. 5065. Springer, 681--700. Google ScholarDigital Library
- ]]Milner, R. 1982. A Calculus of Communicating Systems. Springer. Google ScholarDigital Library
- ]]Padovani, L. 2008. Contract-directed synthesis of simple orchestrators. Proceedings of the 19th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 5201. Springer, 131--146. Google ScholarDigital Library
- ]]Pistore, M., Traverso, P., Bertoli, P., and Marconi, A. 2005. Automated synthesis of composite bpel4ws Web services. In Proceedings of the IEEE International Conference on Web Services (ICWS '05). IEEE Computer Society, 293--301. Google ScholarDigital Library
- ]]Rittri, M. 1993. Retrieving library functions by unifying types modulo linear isomorphism. RAIRO Theor. Informat. Appl. 27, 6, 523--540.Google ScholarCross Ref
- ]]Soloviev, S., Jones, A., and Luo, Z. 1996. Some algorithmic and proof-theoretical aspects of coercive subtyping. Lecture Notes in Computer Science, vol. 1512, Springer, 173--196. Google ScholarDigital Library
- ]]Takeuchi, K., Honda, K., and Kubo, M. 1994. An interaction-based language and its typing system. In Proceedings of the Parallel Architectures and Languages Europe. 398--413. Google ScholarDigital Library
- ]]Traverso, P. and Pistore, M. 2004. Automated composition of semantic Web services into executable processes. In Proceedings of the International Semantic Web Conference. 380--394.Google Scholar
Index Terms
- A theory of contracts for Web services
Recommendations
A theory of contracts for web services
POPL '08Contracts are behavioural descriptions of Web services. We devise a theory of contracts that formalises the compatibility of a client to a service, and the safe replacement of a service with another service. The use of contracts statically ensures the ...
A theory of contracts for web services
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesContracts are behavioural descriptions of Web services. We devise a theory of contracts that formalises the compatibility of a client to a service, and the safe replacement of a service with another service. The use of contracts statically ensures the ...
An algebraic theory for web service contracts
AbstractWe 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 ...
Reviews
Wolfgang Schreiner
In Web-based computing, services and clients must agree on their contract-the order of the messages to be exchanged-in order to have a successful conversation. In particular, it must be possible to decide whether the contract offered by a service is compatible with the contract accepted by a client, or whether one service can be safely replaced by another service that has a different contract. This paper addresses these problems by introducing a subcontract relation between contracts ? and ?, so that every client that complies with the services of ? also complies with the services of ?. One might be tempted to immediately consider every service of ? as a service of ?, but the authors realize that this view leads to a dead end: central properties such as the transitivity of the subcontract relation cannot be established. Therefore, the authors adopt an idea from type theory: a process of ? can be coerced to a process of ? by a filter that removes behaviors not visible in ?. The authors elaborate this idea into a complete theory. Their deduction system yields a subcontract checker that generates a filter between contracts or proves that no filter exists. This enjoyable paper explains the basic intuitive ideas that set the stage for the formal presentations. Although the authors do not elaborate on certain aspects, such as contracts for infinite behaviors, the theory presented in this paper builds a strong basis for further research. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments