We give a formal account of a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocol that services run when invoked (conversation). The calculus includes primitives for defining and for invoking services, for isolating conversations between requesters and providers of services, and primitives for orchestrating services, that is, to make use of existent services as building blocks to accomplish complex tasks. The calculus is equipped with a reduction and a labeled transition semantics; an equivalence result relates the two. To hint how the structuring mechanisms of the language can be exploited for static analysis we present a simple type system guaranteeing the compatibility between client and server protocols, an application of bisimilarity to prove equivalence among services, and we discuss deadlock-avoidance.
Titolo: | Disciplining Orchestration and Conversation in Service-Oriented Computing |
Autore/i: | LANESE, IVAN; VASCONCELOS V. T.; MARTINS F.; RAVARA A. |
Autore/i Unibo: | |
Anno: | 2007 |
Titolo del libro: | Proceedings of SEFM'07, 5th IEEE International Conference on Software Engineering and Formal Methods |
Pagina iniziale: | 305 |
Pagina finale: | 314 |
Digital Object Identifier (DOI): | http://dx.doi.org/10.1109/SEFM.2007.13 |
Abstract: | We give a formal account of a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocol that services run when invoked (conversation). The calculus includes primitives for defining and for invoking services, for isolating conversations between requesters and providers of services, and primitives for orchestrating services, that is, to make use of existent services as building blocks to accomplish complex tasks. The calculus is equipped with a reduction and a labeled transition semantics; an equivalence result relates the two. To hint how the structuring mechanisms of the language can be exploited for static analysis we present a simple type system guaranteeing the compatibility between client and server protocols, an application of bisimilarity to prove equivalence among services, and we discuss deadlock-avoidance. |
Data prodotto definitivo in UGOV: | 26-giu-2013 |
Appare nelle tipologie: | 4.01 Contributo in Atti di convegno |