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.
Disciplining Orchestration and Conversation in Service-Oriented Computing / LANESE I.; VASCONCELOS V.T.; MARTINS F.; RAVARA A.. - STAMPA. - (2007), pp. 305-314. (Intervento presentato al convegno 5th IEEE International Conference on Software Engineering and Formal Methods tenutosi a London, England nel 10-14/09/2007) [10.1109/SEFM.2007.13].
Disciplining Orchestration and Conversation in Service-Oriented Computing
LANESE, IVAN;
2007
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
