publications

2014

1. LNPSE

   Safe Session-Based Service Orchestration with Unreliable Communication

   Jonathan Michaux, Elie Najm, and Alessandro Fantechi

   In Web Services and Formal Methods, 2014

   Abs

   We elaborate on previous work in which we presented SeB, a formalised subset of BPEL extended to support session-based interaction. Sessions are endowed with types that prescribe the correct structure of interactions, and a typed system can be checked for interaction safety. In our previous approach, the communication model was based on reliable FIFO channels, an arguably strong assumption. In this paper, we remove these assumptions and adopt an unreliable and unordered communication model. The contributions of the paper are threefold. Firstly, we propose a model for unordered lossy communication for long-running service interactions. Secondly, we study the effect of this new model on service development, and extend the SeB language and semantics to support message loss and disordering. Finally, we make changes to the session typing system such that our typing discipline now allows us evaluate the interaction-safety of a service configuration in which messages can be lost or arrive in the wrong order.

2013

1. JLAP

   Session types for safe Web service orchestration

   Jonathan Michaux, Elie Najm, and Alessandro Fantechi

   The Journal of Logic and Algebraic Programming, 2013

   Automated Specification and Verification of Web Systems

   Abs

   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.

2. IPTComm

   An Open-Source Platform for Converged Services

   Jonathan Michaux, Emmanuel Buu, Jiri Hlavacek, and 1 more author

   In Proceedings of Principles, Systems and Applications on IP Telecommunications, Oct 2013

   Abs

   Following a telecommunications industry-wide move to provide converged services that integrate solutions from both the Web and the telephony domains, we look in to the challenges in providing adequate environments that foster the creation of these types of services. The challenge in aligning these different service paradigms is that they differ in the way they deal with composition, state management, flow control, and more. Attempts at integrating these different paradigms must do so in a way that encourages the production of high quality code that does not get lost in managing the heterogeneous nature of the underlying resources. We present our experience with the Moteli engine, an open source project that directly addresses these issues.

2012

1. EPTCS

   Adding Sessions to BPEL

   Jonathan Michaux, Elie Najm, and Alessandro Fantechi

   Electronic Proceedings in Theoretical Computer Science, Oct 2012