A theory of contracts for Web services

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.

REFERENCES

• 1: 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.
• 2: J. C. M. Baeten , F. Corradini , C. A. Grabmayer, A characterization of regular expressions under bisimulation, Journal of the ACM (JACM), v.54 n.2, p.6-es, April 2007 [doi>10.1145/1219092.1219094]
• 3: 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.
• 4: 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.
• 5: 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.
• 6: 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.
• 7: 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.
• 8: Ed Brinksma , Giuseppe Scollo , Chris Steenbergen, Lotos specifications, their implementations and their tests, Conformance testing methodologies and architectures for OSI protocols, IEEE Computer Society Press, Los Alamitos, CA, 1995
• 9: Kim B. Bruce , Giuseppe Longo, A modest model of records, inheritance, and unbounded quantification, Information and Computation, v.87 n.1-2, p.196-240, July/August 1990 [doi>10.1016/0890-5401(90)90062-M]
• 10: Marco Carbone , Kohei Honda , Nobuko Yoshida, A Calculus of Global Interaction based on Session Types, Electronic Notes in Theoretical Computer Science (ENTCS), v.171 n.3, p.127-151, June, 2007 [doi>10.1016/j.entcs.2006.12.041]
• 11: 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.
• 12: Luca Cardelli, A semantics of multiple inheritance, Information and Computation, v.76 n.2-3, p.138-164, February/March 1988 [doi>10.1016/0890-5401(88)90007-7]
• 13: 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.
• 14: 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.
• 15: Giuseppe Castagna , Alain Frisch, A gentle introduction to semantic subtyping, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.198-199, July 11-13, 2005, Lisbon, Portugal [doi>10.1145/1069774.1069793]
• 16: Giuseppe Castagna , Nils Gesbert , Luca Padovani, A theory of contracts for web services, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 17: Giuseppe Castagna , Nils Gesbert , Luca Padovani, A theory of contracts for web services, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 18: Gang Chen, Soundness of Coercion in the Calculus of Constructions, Journal of Logic and Computation, v.14 n.3, p.405-427, June 2004 [doi>10.1093/logcom/14.3.405]
• 19: 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/.
• 20: 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/.
• 21: Courcelle, B. 1983. Fundamental properties of infinite trees. Theor. Comput. Sci. 25, 95--169.
• 22: 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.
• 23: De Nicola, R. and Hennessy, M. 1984. Testing equivalences for processes. Theor. Comput. Sci. 34, 83--133.
• 24: R. De Nicola , M. Hannessy, CCS without &tgr;'s, The International Joint Conference on theory and practice of software development on TAPSOFT '87, p.138-152, January 1987, Pisa, Italy
• 25: Rocco De Nicola , Anna Labella, Nondeterministic regular expressions as solutions of equational systems, Theoretical Computer Science, v.302 n.1-3, p.179-189, 13 June 2003 [doi>10.1016/S0304-3975(02)00774-0]
• 26: J. Derrick , H. Bowman , E. A. Boiten , M. W. A. Steen, Comparing LOTOS and Z refinement relations, IFIP TC6/ 6.1 international conference on formal description techniques IX/protocol specification, testing and verification XVI on Formal description techniques IX : theory, application and tools: theory, application and tools, p.501-516, January 1996, Kaiserslautern, Germany
• 27: Roberto Di Cosmo, Isomorphisms of types: from &lgr;-calculus to information retrieval and language design, Birkhauser Verlag, Basel, Switzerland, 1995
• 28: Fallside, D. C. and Walmsley, P. 2004. XML Schema part 0: Primer second edition. W3C Recommendation, http://www.w3.org/TR/xmlschema-0/.
• 29: Cédric Fournet , Georges Gonthier, The reflexive CHAM and the join-calculus, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.372-385, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237805]
• 30: Cédric Fournet , Georges Gonthier , Jean-Jacques Lévy , Luc Maranget , Didier Rémy, A Calculus of Mobile Agents, Proceedings of the 7th International Conference on Concurrency Theory, p.406-421, August 26-29, 1996
• 31: 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.
• 32: Alain Frisch , Giuseppe Castagna , Véronique Benzaken, Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types, Journal of the ACM (JACM), v.55 n.4, p.1-64, September 2008 [doi>10.1145/1391289.1391293]
• 33: Simon Gay , Malcolm Hole, Subtyping for session types in the pi calculus, Acta Informatica, v.42 n.2, p.191-225, November 2005 [doi>10.1007/s00236-005-0177-z]
• 34: M. Hennessy, Acceptance trees, Journal of the ACM (JACM), v.32 n.4, p.896-928, Oct. 1985 [doi>10.1145/4221.4249]
• 35: Matthew Hennessy, Algebraic theory of processes, MIT Press, Cambridge, MA, 1988
• 36: Kohei Honda, Types for Dynamic Interaction, Proceedings of the 4th International Conference on Concurrency Theory, p.509-523, August 23-26, 1993
• 37: Kohei Honda , Vasco Thudichum Vasconcelos , Makoto Kubo, Language Primitives and Type Discipline for Structured Communication-Based Programming, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.122-138, March 28-April 04, 1998
• 38: Richard Hull , Michael Benedikt , Vassilis Christophides , Jianwen Su, E-services: a look behind the curtain, Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, p.1-14, June 09-11, 2003, San Diego, California [doi>10.1145/773153.773154]
• 39: 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.
• 40: Cosimo Laneve , Luca Padovani, The Must Preorder Revisited, Proceedings of the 18th international conference on Concurrency Theory, September 03-08, 2007, Lisbon, Portugal [doi>10.1007/978-3-540-74407-8_15]
• 41: Cosimo Laneve , Luca Padovani, The Pairing of Contracts and Session Types, Concurrency, Graphs and Models: Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, Springer-Verlag, Berlin, Heidelberg, 2008 [doi>10.1007/978-3-540-68679-8_42]
• 42: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 43: Luca Padovani, Contract-Directed Synthesis of Simple Orchestrators, Proceedings of the 19th international conference on Concurrency Theory, August 19-22, 2008, Toronto, Canada [doi>10.1007/978-3-540-85361-9_13]
• 44: M. Pistore , P. Traverso , P. Bertoli , A. Marconi, Automated Synthesis of Composite BPEL4WS Web Services, Proceedings of the IEEE International Conference on Web Services, p.293-301, July 11-15, 2005 [doi>10.1109/ICWS.2005.27]
• 45: Rittri, M. 1993. Retrieving library functions by unifying types modulo linear isomorphism. RAIRO Theor. Informat. Appl. 27, 6, 523--540.
• 46: Alex Jones , Zhaohui Luo , Sergei Soloviev, Some Algorithmic and Proof-Theoretical Aspects of Coercive Subtyping, Selected papers from the International Workshop on Types for Proofs and Programs, p.173-195, December 15-19, 1996
• 47: Kaku Takeuchi , Kohei Honda , Makoto Kubo, An Interaction-based Language and its Typing System, Proceedings of the 6th International PARLE Conference on Parallel Architectures and Languages Europe, p.398-413, July 04-08, 1994
• 48: 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.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

  H. Information Systems
  H.3 INFORMATION STORAGE AND RETRIEVAL
      H.3.5 On-line Information Services
          Subjects: Web-based services
  H.5 INFORMATION INTERFACES AND PRESENTATION (I.7)
      H.5.3 Group and Organization Interfaces
          Subjects: Web-based interaction; Theory and models

General Terms:
Languages, Standardization, Theory

Keywords:
Web services, ccs, concurrency theory, contracts, explicit coercions, must testing, subtyping, type theory