Choreographic Programming is a correct-by-construction paradigm where a compilation procedure synthesises deadlock-free, concurrent, and distributed communicating processes from global, declarative descriptions of communications, called choreographies. Previous work used choreographies for the synthesis of programs. Alas, there is no formalisation that provides a chain of correctness from choreographies to their implementations. This problem originates from the gap between existing theoretical models, which abstract communications using channel names (`a la CCS/{pi}-calculus), and their implementations, which use low-level mechanisms for message routing. As a solution, we propose the theoretical framework of Applied Choreographies. In the framework, developers write choreographies in a language that follows the standard syntax and name-based communication semantics of previous works. Then, they use a compilation procedure to transform a choreography into a low-level, implementation-adherent calculus of Service-Oriented Computing (SOC). To manage the complexity of the compilation, we divide its formalisation and proof in three stages, respectively dealing with: a) the translation of name-based communications into their SOC equivalents (namely, using correlation mechanisms based on message data); b) the projection of a choreography into a composition of partial, single-participant choreographies (towards their translation into SOC processes); c) the translation of partial choreographies and the distribution of choreography-level state into SOC processes. We provide results of behavioural correspondence for each stage. Thus, given a choreography specification, we guarantee to synthesise its faithful and deadlock-free service-oriented implementation.
Download