Real-World Choreographies

Giallorenzo, Saverio (2016) Real-World Choreographies, [Dissertation thesis], Alma Mater Studiorum Università di Bologna. Dottorato di ricerca in Informatica, 28 Ciclo. DOI 10.6092/unibo/amsdottorato/7512.
Documenti full-text disponibili:
Documento PDF (English) - Richiede un lettore di PDF come Xpdf o Adobe Acrobat Reader
Download (1MB) | Anteprima


Choreographies are a relatively new tool for designing distributed systems from a global viewpoint. Moreover, choreographies are also free from deadlocks and race conditions by design. Recent theoretical results defined proper Endpoint Projection (EPP) functions to compile choreographic specifications into their single components. Since EPPs are behavioural preserving, projected systems also enjoy freedom from deadlocks and races by construction. Aim of this PhD is to formalise non-trivial features of distributed systems with choreographies and to translate our theoretical results into the practice of implemented systems. To this purpose, we provide two main contributions. The first contribution tackles one of the most challenging features of distributed development: programming correct and consistent runtime updates of distributed systems. Our solution is a theoretical model of dynamic choreographies that provides a clear definition of which components and behaviours can be updated. We prove that compiled choreographic specifications are correct and consistent after any update. We also refine our theoretical model to provide a finer control over updates. On this refinement, we develop a framework for programming adaptable distributed systems. The second contribution covers one of the main issues of implementing theoretical results on choreographies: formalising the compilation from choreographies to executable programs. There is a sensible departure between the present choreographic frameworks and their theoretical models because their theories abstract communications with synchronisation on names (a la CCS/π-calculus) yet they compile to Jolie programs, an executable language that uses correlation — a renown technology of Service-Oriented Computing — for message routing. Our solution is a theory of Applied Choreographies (AC) that models correlation-based message passing. We pinpoint the key theoretical problems and formalise the principles that developers should follow to obtain correct implementations. Finally, we prove our approach by defining a correct compiler from AC to the calculus behind the Jolie language.

Tipologia del documento
Tesi di dottorato
Giallorenzo, Saverio
Dottorato di ricerca
Scuola di dottorato
Scienze e ingegneria dell'informazione
Settore disciplinare
Settore concorsuale
Parole chiave
Distributed Systems, Choreographies, Dynamic Updates, Adaptation, Service-Oriented Computing, Process Calculi, Session Types
Data di discussione
12 Maggio 2016

Altri metadati

Statistica sui download

Gestione del documento: Visualizza la tesi