PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Michaux J., Najm E., Fantechi A. Session types for safe Web service orchestration. In: Journal of Logic and Algebraic Programming, vol. 82 (8) pp. 282 - 310. Elsevier, 2013.
 
 
Abstract
(English)
We address the general problem of interaction safety in Web service orchestrations. By considering an essential subset of the BPEL orchestration language, we define SeB, a session based style of this subset. We discuss the formal semantics of SeB and present its main properties. We take a new approach to address the formal semantics which is based on a translation into so-called control graphs. Our semantics accounts for BPEL control links and addresses the static semantics that prescribes the valid usage of variables. We also provide the semantics of service configurations. During a session, a client and a service can engage in a complex series of interactions. By means of the provided semantics, we define precisely what is meant by interaction safety. We then introduce session types in order to prescribe the correct orderings of these interactions. Service providers must declare their provided and required session types. We define a typing algorithm that checks if a service orchestration behaves according to its declared provided and required types. Using a subtyping relation defined on session types, we show that any configuration of well-typed service partners with compatible session types are interaction safe, i.e., involved partners never receive unexpected messages.
URL: http://www.sciencedirect.com/science/article/pii/S1567832613000271
DOI: 10.1016/j.jlap.2013.05.004
Subject Session types
Orchestration
Web services
BPEL
Interaction-safety
Behavioural compatibility
C.2.4 Distributed Systems
D.2.4 Software/Program Verification


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional