On the Synthesis of Choreographies

The theories based on session types stand out as effective methodologies to specify and verify properties of distributed systems. A key result in the area shows the suitability of choreography languages and session types as a basis for a choreography-driven methodology for distributed software development. The methodology it advocates is as follows: a team of programmers designs a global view of the interactions to be implemented (i.e., a choreography), then the choreography is projected onto each role. Finally, each program implementing one or more roles in the choreography is validated against its corresponding projection(s). This is an ideal methodology but it may not always be possible to design one set of choreographies that will drive the overall development of a distributed system. Indeed, software needs maintenance, specifications may evolve (sometimes also during the development), and issues may arise during the implementation phase. Therefore, there is a need for an alternative approach whereby it is possible to infer a choreography from local behavioural specifications (i.e., session types). We tackle the problem of synthesising choreographies from local behavioural specifications by introducing a type system which assigns – if possible – a choreography to set of session types. We demonstrate the importance of obtaining a choreography from local specifications through two applications. Firstly, we give three algorithms and a methodology to help software designers refine a choreography into a global assertion, i.e., a choreography decorated with logical formulae specifying senders’ obligations and receivers’ requirements. Secondly, we introduce a formal model for distributed systems where each participant advertises its requirements and obligations as behavioural contracts (in the form of session types), and where multiparty sessions are started when a set of contracts allows to synthesise a choreography.