Session types for safe Web service orchestration

• We give a novel formal semantics of the BPEL orchestration language.
• We extend BPEL to support sessions.
• We provide behavioural typing of services by using typed sessions.
• We provide a solution to check the well-typedness of services and service configurations.
• We prove the property of safe interaction for well-typed service configurations.

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.