CastagnaGesbertPadovani08 (In proceedings)
|
Author(s) | Giuseppe Castagna, Nils Gesbert and Luca Padovani |
Title | « A Theory of Contracts for Web Services » |
In | Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08) |
Series | ACM SIGPLAN Notices |
Volume | 43 |
Page(s) | 261-272 |
Year | 2008 |
Publisher | ACM |
URL | http://www.di.unito.it/~padovani/Papers/filtered_contracts.pdf |
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. |
@inproceedings{CastagnaGesbertPadovani08,
volume = {43},
author = {Giuseppe Castagna and Nils Gesbert and Luca Padovani},
issue = {1},
series = {ACM SIGPLAN Notices},
booktitle = {Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages (POPL'08)},
url = {http://www.di.unito.it/~padovani/Papers/filtered_contracts.pdf},
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. },
title = {{A Theory of Contracts for Web Services}},
publisher = {ACM},
doi = {10.1145/1328438.1328471},
year = {2008},
pages = {261-272},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)