M.: Towards a Formal Model for Agile Service Discovery and Integration

Abstract. As the fundamental web services technologies are becoming mature, web service composition, orchestration and choreography are gaining increasing attention. The movement from static interactions be-tween already known partners as in BPEL to dynamically discovered and agile business partners is irresistible facing ever changing environ-ments while aiming for specifically optimized collaborations. However, the techniques and models currently used lack fundamental formal foun-dations making them inadequate especially for modeling non-functional aspects. As a step toward the vision of dynamically discovered and ag-ile processes, this paper proposes a formal approach to unambiguously define the syntax of service orchestrations and choreographies by repre-senting key elements of service–oriented computing in a process algebra, the pi-calculus. The results include a formal description of correlations in the context of service choreography as well as a formal representation of an orchestration pattern derived from BPMN and BPEL. The results provide a better understanding of service-based processes in terms of a formal algebra that will open the door for automated discovery and bind-ing of potential business partners via service equivalence and mobility.