MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Compositional Choreographies
Fabrizio MONTESI , Nobuko YOSHIDA
24th International Conference on Concurrency Theory (CONCUR 2013) p. 439 - 425

Choreography-based programming is a powerful paradigm for designing communicating systems, where the flow of communications between peers (endpoints) is specified with a global description. Due to their global nature, current choreography models can specify only the behaviour of closed systems, i.e., systems where the behaviour of all endpoints is known at design time. This limitation prevents the usage of choreographies in real-world distributed scenarios where the ability to compose different systems whose implementation details are unknown (as \“black boxes\“) can be crucial. This paper proposes a new model that supports a compositionality of choreographies. The key of our approach is the introduction of partial choreographies, which can mix global descriptions with communications among external peers. We prove that if two choreographies are composable, then the endpoints independently generated from each choreography are also composable, preserving their typability and deadlock-freedom. The usability of our framework is demonstrated by modelling an industrial use case implemented in a framework for Web Services, Jolie.

@inproceedings{MY2013,
  author = {Fabrizio Montesi and Nobuko Yoshida},
  title = {{Compositional Choreographies}},
  series = {LNCS},
  volume = {8052},
  pages = {439--425},
  publisher = {Springer},
  year = 2013
}
@inproceedings{MY2013,
  author = {Fabrizio Montesi and Nobuko Yoshida},
  title = {{Compositional Choreographies}},
  booktitle = {24th International Conference on Concurrency Theory},
  series = {LNCS},
  volume = {8052},
  pages = {439--425},
  publisher = {Springer},
  doi = "10.1007/978-3-642-40184-8_30",
  year = 2013
}