Formal Methods for Communication Protocols

Course on the TNE-Desk project
This course presents basic ideas of some formal behavioural specifications used in academia and industry. The course is designed to be accessible to master and PhD students; many concepts are presented informally, yet precisely. The overall topic of the course regards some recent formal models proposed for distributed coordination and based choreographic approaches. The first model is based on a variant of multiparty session types [1], a pretty successful model for the design and analysis of communication protocols. The second model advocates local-first principles for communication protocols and departs from multiparty session types in several ways [2,3]. In the final part of the course we will consider an actor model featuring join patterns, a programming constructs that allows the straightforward realisation of complex coordination policies. Surprisingly, join patterns [4,5] have an application in computational economy; in fact we will see how they can be used to implement the design of on-line market designs.

Lecture notes:

Further readings:

• [1] K. Honda, N. Yoshida and M. Carbone. Multiparty Asynchronous Session Types. JACM 63(1), 2016.
• [2] R. Kuhn, H. C. Melgratti and E. Tuosto. Behavioural Types for Local-First Software. ECOOP 2023
• [3] R. Kuhn, H. C. Melgratti and E. Tuosto. Behavioural Types for Local-First Software (Artifact). Dagstuhl Artifacts Ser. 2023
• [4] C. Fournet and G. Gonthier. The Reflexive CHAM and the Join-Calculus. POPL’96
• [5] A. J. Turon, C. V. Russo. Scalable join patterns. SPLASH 2011
• [6] Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, USA, 1986.
• [7] D. Brand and P. Zafiropulo. On Communicating Finite-State Machines. JACM, 30(2):323–342, 1983.
• [8] P. Deniélou and N. Yoshida. Multiparty session types meet communicating automata. In ESOP 2012.
• [9] C. Hewitt, P. B. Bishop, and R. Steiger. A Universal Modular ACTOR Formalism for Artificial Intelligence. IJCAI, 1973.
• [6] N. Kavantzas, D. Burdett, G. Ritzinger, T. Fletcher, and Y. Lafon. Web services choreography description language version 1.0. http://www.w3.org/TR/2004/WD-ws-cdl-10-20041217. Working Draft 17 December 2004.