Type Systems for Distributed Programs: Components and Sessions

Dardha, Ornela (2014) Type Systems for Distributed Programs: Components and Sessions, [Dissertation thesis], Alma Mater Studiorum Università di Bologna. Dottorato di ricerca in Informatica, 26 Ciclo. DOI 10.6092/unibo/amsdottorato/6441.
Documenti full-text disponibili:
[img]
Anteprima
Documento PDF (English) - Richiede un lettore di PDF come Xpdf o Adobe Acrobat Reader
Download (869kB) | Anteprima

Abstract

Modern software systems, in particular distributed ones, are everywhere around us and are at the basis of our everyday activities. Hence, guaranteeing their cor- rectness, consistency and safety is of paramount importance. Their complexity makes the verification of such properties a very challenging task. It is natural to expect that these systems are reliable and above all usable. i) In order to be reliable, compositional models of software systems need to account for consistent dynamic reconfiguration, i.e., changing at runtime the communication patterns of a program. ii) In order to be useful, compositional models of software systems need to account for interaction, which can be seen as communication patterns among components which collaborate together to achieve a common task. The aim of the Ph.D. was to develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems appeared to be an adequate methodology, considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like, deadlock or livelock freedom in a concurrent setting. The main contributions of this dissertation are twofold. i) On the components side: we design types and a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations related to modifications of communication patterns in a program during execution time. ii) On the communication side: we study advanced safety properties related to communication in complex distributed systems like deadlock-freedom, livelock- freedom and progress. Most importantly, we exploit an encoding of types and terms of a typical distributed language, session π-calculus, into the standard typed π- calculus, in order to understand their expressive power.

Abstract
Tipologia del documento
Tesi di dottorato
Autore
Dardha, Ornela
Supervisore
Dottorato di ricerca
Scuola di dottorato
Scienze e ingegneria dell'informazione
Ciclo
26
Coordinatore
Settore disciplinare
Settore concorsuale
Parole chiave
components, distributed systems, concurrency, π- calculus, session types, encoding, progress, lock-freedom.
URN:NBN
DOI
10.6092/unibo/amsdottorato/6441
Data di discussione
19 Maggio 2014
URI

Altri metadati

Statistica sui download

Gestione del documento: Visualizza la tesi

^