Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/29310
Title: On the Synthesis of Choreographies
Authors: Lange, Julien
Supervisors: Tuosto, Emilio
Crole, Roy
Award date: 1-Dec-2013
Presented at: University of Leicester
Abstract: 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.
Links: http://hdl.handle.net/2381/29310
Type: Thesis
Level: Doctoral
Qualification: PhD
Rights: Copyright © the author. All rights reserved.
Appears in Collections:Theses, Dept. of Computer Science
Leicester Theses

Files in This Item:
File Description SizeFormat 
2013LangeJPhD.pdf822.85 kBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.