PhD course: Distributed applications with automata and choreographies

Post date: 25-Jun-2015 16:28:11

Upcoming PhD course

Designing and analysing distributed applications with automata and choreographies

July 2015

Dipartimento di Matematica e Informatica - Via Ospedale 72, Cagliari

Emilio Tuosto

University of Leicester, UK

Abstract.

This series of lectures will touch upon recent developements in the research on the rigorous design and analysis of distributed applications. The focus will be on the so called communication-centric applications. Such applications are nowadays paramount; it is indeed hard to imagine stand-alone closed applications (or programming languages) that do not offer mechanisms for smooth integration. Such mechanisms can be suitably abstracted in terms of communications. The paradigm of service-oriented and cloud-computing begin the paradigmatic specimen of this application domain.

Firstly, we will introduce communicating finite state machines (CFSM for short), a well known model introduced as a specification language of distributed protocols featuring message passing. This model has been recently proved expressive enough (in fact, a generalisation of) session types, which provide a state-of-the-art theory for specifying and analysing communication-centric applications.

Secondly, we will explore choreography-based design of distributed applications. For this we will use global graphs (GG, for short) a concrete design visual language which allows to explicitly represent points of distributed choice as well as parallel computations. We will discuss how GG can be used to design communication-centric applications.

Thirdly, we will consider the relations among CFSM and GG. More precisely we will see how to (algorithmically) transform GG into CFSM as well as (sets of) CFSM into GG. This will allow us to speculate on how such algorithms could be used in the software development cycle to attain robust distributed applications.

The lectures will be supported by a tool which will be used during lectures and in a few lab sessions as didactic support of the topics covered in the lectures.

Course schedule.

The official presentation of the course will be on June 30 (Tuesday) in Aula F, at 11:00. The schedule of the course will be fixed during this meeting. The course will be taught in english.

  • Tuesday 30 (June), 11.00-13.00 Aula F [Motivations]
  • Wednesday 1 (July), 11.00-13.00 Aula D
  • Thursday 2, 11.00-13.00 Aula F
  • Friday 3, 14.00-16.00 Aula F
  • Tuesday 7 (July), 11.00-13.00 Aula F
  • Thursday 9, 11.00-13.00 Aula C
  • Friday 10, 11.00-13.00 Aula F
  • Monday 13, 11.00-13.00 Aula F
  • Tuesday 14, 11.00-13.00 Aula C
  • Wednesday 15, 11.00-13.00 Aula C

References.

  1. Kohei Honda, Nobuko Yoshida, Marco Carbone. Multiparty asynchronous session types. POPL 2008
  2. Julien Lange, Emilio Tuosto, Nobuko Yoshida. From Communicating Machines to Graphical Choreographies. POPL 2015
  3. Daniel Brand, Pitro Zafiropulo. On Communicating Finite-State Machines. J. ACM 30(2): 323-342 (1983)
  4. Julien Lange, Emilio Tuosto. GMC Synthesis tool.