| Abstract |
| Contracts are behavioral descriptions of Web services. We devise a theory of contracts that formalizes 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 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. |
@article{CastagnaGesbertPadovani09,
number = {5},
volume = {31},
issn = {0164-0925},
author = {Giuseppe Castagna and Nils Gesbert and Luca Padovani},
url = {http://www.di.unito.it/~padovani/Papers/filtered_contracts_journal.pdf},
abstract = { Contracts are behavioral descriptions of Web services. We devise
a theory of contracts that formalizes 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 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. },
title = {{A Theory of Contracts for Web Services}},
publisher = {ACM},
year = {2009},
doi = {10.1145/1538917.1538920},
journal = {ACM Transactions on Programming Languages and Systems},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
