Related to “UBA, ULEIC, and AAU will adapt algorithms for synthesising choreographies that take into account rely-guarantee contracts and use synthesis techniques for refinement of specifications from composite models.”

We addressed the problem of synthesising choreographies from local descriptions that provide information about the data exchanged during the communication. Technically, we consider local behaviours described as guarded communicating machine in which input and output actions are associated with enabling conditions in a logical language. We worked on reducing the problem to a combination of existing synthesis algorithm for communicating machines having no data annotations, and  use entailment relation for a logical language. 

In addition, we developed a language for data-driven global specifications based on distributed tuple spaces. 

These specifications, akin behavioural types, describe the coordination from a global point of view. Our specifications express the data flow across distributed tuple spaces rather than detailing the communication pattern of processes. We devised a typing system to validate Klaim programs against projections of our global specifications. An interesting feature of our typing approach is that well-typed systems have an arbitrary number of participants.

Results of this task  appear in:
Roberto Bruni, Andrea Corradini, Fabio Gadducci, Hernán C. Melgratti, Ugo Montanari, Emilio Tuosto. Data-driven choreographies à la Klaim. Lecture Notes in Computer Science 11665, 2019.