As the adoption of SOA grows in enterprises and businesses and more and more complex information systems are reworked or designed anew on the basis of the emerging service-oriented paradigm, the complexity of the conversations that take place among services provided by the different players magnifies accordingly. Connecting complex services by “pairing” them on a one-to-one basis does not suffice any longer. Instead, it becomes critical to support complex, possibly long-lasting multi-party conversations involving a diversity of services. Operations exposed by the services can not any longer be restricted to only a service provider and a service requester, but have to scope up to a multi-party environment in which each service describes how it can consume and produce messages in conversations involving arbitrary numbers of participants.

The research community is investigating the formalisms best suited to this task, which are collectively called business protocol languages. Proposals for business protocol languages range from adapted business process languages like BPELlight, to more formal approaches based on π-calculus, Deterministic Finite Automata (DFA) and Petri-Nets.

Conversations can be structured either as orchestrations that describe the local point of view of one of the participants (called subject), or as choreographies that provide the global point of view, in which all the different participants are inter-connected. Unfortunately, none of the business protocol languages proposed so far leverages effectively orchestrations and choreographies, but instead they all focus on either. Relating orchestrations and choreographies is instrumental to the bigger picture of business protocol evolution, the evolving of business protocol models to address mutated or emerging requirements such as changes to the behavior of partners, KPIs and QoS parameters to be met, and so on.

The talk will describe a formal meta-model for representing business protocols using Deterministic Finite Automata enriched with time conditions on the transitions. The running example will be a complex multi-party conversation. On top of the running example we will present a set of soundness properties for choreography business protocol models: time-soundness, participant-soundness and full-soundness. The soundness properties are crucial for choreography business protocols to be used in distributed environments. For instance, the full-soundness property guarantees the progression of the execution of business protocol instances.