A Theory of Contracts for Web Services
A Theory of Contracts for Web Services
复制标题
DOI：
10.1145/1538917.1538920
复制
发表时间：
2009-06-01
影响因子：
1.3
通讯作者：
Padovani, Luca
中科院分区：
文献类型：
--
作者：
Castagna, Giuseppe;Gesbert, Nils;Padovani, Luca
契约是Web服务的行为描述。我们设计了一个契约理论，它正式化了客户端与服务的兼容性，以及用另一个服务安全地替换一个服务。契约的使用静态地确保了兼容客户端和服务之间的每一个可能的交互的成功完成。该理论的技术设备是过滤器，这是一种明确的强制，防止服务的某些可能行为，并在这样做的过程中，使服务兼容不同的使用场景。我们发现，过滤器可以被看作是一个健全的和完整的分包演绎系统，同时完善和扩展轩尼诗的经典公理化必须测试前序的证明。这种关系是可判定的，决策算法是通过切割消除过程来获得的，该过程证明了分包作为一个逻辑系统的一致性。尽管技术发展非常丰富，但最终的方法是基于简单的思想和基本的直觉。值得注意的是，它的应用程序大多独立于用于编程服务或客户端的语言。我们概述了我们的理论的实际方面，通过研究两种不同的具体合同语法，并将它们应用到Web服务语言。我们还探讨了过滤器的实现问题，并讨论了未来研究的前景，这项工作打开。
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.