Session types for orchestration charts

We introduce an approach for verifying service composition based on behavioral typing. Sessions play a pivotal role in this approach. Sessions are the quanta of service delivery. A session is a sequence of interactions between a service provider and a service requestor that starts with a service invocation message sent by the requestor. Sessions generalize the request/response interaction paradigm allowing for more complex interaction patterns. A session is sound when both the requestor and the provider behave in mutual conformance. A collection of interacting services is sound when all the sessions that can be initiated and executed by this collection are sound. Our approach is based on two (graphical) languages: OrCharts - that allow to define and orchestrate session based services; and TypeCharts - that allow to define behavioral types for service sessions. We provide a typing algorithm and discuss the properties that are verified in well typed services. In this work we sought for a service orchestration language that is expressive but still simple enough to allow for typing and service compatibility verification. We show also that the language allows to express many common orchestration examples.