A theory of contracts for web services

ABSTRACT

Contracts 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 successful completion of every possible interaction between compatible clients and services.

The technical device that underlies the theory is the definition of filters, which are explicit coercions that prevent some possible behaviours of services and, in doing so, they 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 axiomatisation 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 also outline the possible practical impact of such a work and the perspectives of future research it opens.

REFERENCES

• 1: A. Alves, A. Arkin, S. Askary, C. Barreto, et al. Web Services Business Process Execution Language Version 2.0, April 2007. OASIS Standard, http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html.
• 2: A. Banerji, C. Bartolini, D. Beringer, V. Chopella, et al. Web Services Conversation Language (wscl) 1.0, March 2002. W3C Note, http://www.w3.org/TR/2002/NOTE-wscl10-20020314.
• 3: T. Bellwood, S. Capell, L. Clement, J. Colgrave, et al. UDDI Version 3.0.2, 2005. OASIS Standard, http://uddi.org/pubs/uddi-v3.0.2-20041019.htm.
• 4: M. Bravetti and G. Zavattaro. Towards a unifying theory for choreography conformance and contract compliance. In Proc. of the 6th Intl. Symposium on Software Composition. Springer, 2007.
• 5: 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]
• 6: 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]
• 7: M. Carbone, K. Honda, and N. Yoshida. Structured communication-centred programming for web services. In ESOP'07, 16th European Symposium on Programming, LNCS 4421. Springer, 2007b.
• 8: 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]
• 9: S. Carpineti, G. Castagna, C. Laneve, and L. Padovani. A formal account of contracts for Web Services. In 3rd Int'l Workshop on Web Services and Formal Methods, LNCS 4184. Springer, 2006.
• 10: 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]
• 11: 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
• 12: 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]
• 13: R. Chinnici, J.-J. Moreau, A. Ryman, and S. Weerawarana. Web Services Description Language (wsdl) Version 2.0 Part 1: Core Language, June 2007b. W3C Recommendation, http://www.w3.org/TR/wsdl20/.
• 14: R. Chinnici, H. Haas, A.-A. Lewis, J.-J. Moreau, et al. Web Services Description Language (wsdl) Version 2.0 Part 2: Adjuncts, June 2007a. W3C Recommendation, http://www.w3.org/TR/wsdl20-adjuncts/.
• 15: 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
• 16: R. De Nicola and M. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83--133, 1984.
• 17: Roberto Di Cosmo, Isomorphisms of types: from &lgr;-calculus to information retrieval and language design, Birkhauser Verlag, Basel, Switzerland, 1995
• 18: D. C. Fallside and P. Walmsley. XML Schema Part 0: Primer Second Edition, October 2004. W3C Recommendation, http://www.w3.org/TR/xmlschema-0/.
• 19: C. Fournet, C. A. R. Hoare, S. K. Rajamani, and J. Rehof. Stuck-free conformance. In CAV'04, LNCS 3114. Springer, 2004.
• 20: 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]
• 21: Matthew Hennessy, Algebraic theory of processes, MIT Press, Cambridge, MA, 1988
• 22: M. Hennessy, Acceptance trees, Journal of the ACM (JACM), v.32 n.4, p.896-928, Oct. 1985 [doi>10.1145/4221.4249]
• 23: Kohei Honda, Types for Dynamic Interaction, Proceedings of the 4th International Conference on Concurrency Theory, p.509-523, August 23-26, 1993
• 24: 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
• 25: C. Laneve and L. Padovani. The must preorder revisited -- An algebraic theory for web services contracts. In 18th International Conference on Concurrency Theory. LNCS 4703, Springer, 2007.
• 26: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 27: M. Rittri. Retrieving library functions by unifying types modulo linear isomorphism. RAIRO Theoretical Informatics and Applications, 27(6):523--540, 1993.
• 28: 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
• 29: 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

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

General Terms:
Languages, Standardization, Theory

Keywords:
CCS, concurrency theory, contracts, explicit coercions, must testing, subtyping, type theory, web services