An algebraic theory for web service contracts

Verfasser / Beitragende:
[Cosimo Laneve, Luca Padovani]
Ort, Verlag, Jahr:
2015
Enthalten in:
Formal Aspects of Computing, 27/4(2015-07-01), 613-640
Format:
Artikel (online)
ID: 605516367
LEADER caa a22 4500
001 605516367
003 CHVBK
005 20210128100713.0
007 cr unu---uuuuu
008 210128e20150701xx s 000 0 eng
024 7 0 |a 10.1007/s00165-015-0334-2  |2 doi 
035 |a (NATIONALLICENCE)springer-10.1007/s00165-015-0334-2 
245 0 3 |a An algebraic theory for web service contracts  |h [Elektronische Daten]  |c [Cosimo Laneve, Luca Padovani] 
520 3 |a We study the foundations of Web service technologies for connecting abstract and concrete service definitions and for discovering services according to their observable behavior. We pursue this study addressing a subset of BPEL activities that include concurrency constructs. We present a formal semantics—called compliance preorder—of this subset of BPEL and we define a behavioral type discipline that guarantees the correctness of client-server interactions. The types of our discipline, called contracts, are De Nicola and Hennessy tau-less, finite-state CCS processes. We show that contracts are BPEL normal forms according to the compliance preorder and that the compliance preorder does coincide with a well-known equivalence in concurrency theory, the must-testing preorder. The compliace preorder is not fully adequate for discovering Web services though, since it does not support width and depth extensions of Web services. To address this issue, we propose a sound generalization of the compliance preorder, called subcontract relation, that admits a notion of principal service contract—the dual contract—compliant with a given client contract and that exhibits good precongruence properties when choreographies of Web services are considered. 
540 |a British Computer Society, 2015 
690 7 |a Web services  |2 nationallicence 
690 7 |a BPEL  |2 nationallicence 
690 7 |a Contracts  |2 nationallicence 
690 7 |a Compliance  |2 nationallicence 
690 7 |a Must-testing  |2 nationallicence 
690 7 |a Subcontract  |2 nationallicence 
690 7 |a Dual contract  |2 nationallicence 
690 7 |a Choreography  |2 nationallicence 
700 1 |a Laneve  |D Cosimo  |u Dipartimento di Informatica - Scienza e Ingegneria, Università di Bologna, Bologna, Italy  |4 aut 
700 1 |a Padovani  |D Luca  |u Dipartimento di Informatica, Università di Torino, Turin, Italy  |4 aut 
773 0 |t Formal Aspects of Computing  |d Springer London  |g 27/4(2015-07-01), 613-640  |x 0934-5043  |q 27:4<613  |1 2015  |2 27  |o 165 
856 4 0 |u https://doi.org/10.1007/s00165-015-0334-2  |q text/html  |z Onlinezugriff via DOI 
898 |a BK010053  |b XK010053  |c XK010000 
900 7 |a Metadata rights reserved  |b Springer special CC-BY-NC licence  |2 nationallicence 
908 |D 1  |a research-article  |2 jats 
949 |B NATIONALLICENCE  |F NATIONALLICENCE  |b NL-springer 
950 |B NATIONALLICENCE  |P 856  |E 40  |u https://doi.org/10.1007/s00165-015-0334-2  |q text/html  |z Onlinezugriff via DOI 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Laneve  |D Cosimo  |u Dipartimento di Informatica - Scienza e Ingegneria, Università di Bologna, Bologna, Italy  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Padovani  |D Luca  |u Dipartimento di Informatica, Università di Torino, Turin, Italy  |4 aut 
950 |B NATIONALLICENCE  |P 773  |E 0-  |t Formal Aspects of Computing  |d Springer London  |g 27/4(2015-07-01), 613-640  |x 0934-5043  |q 27:4<613  |1 2015  |2 27  |o 165