Guess Who’s Coming: Runtime Inclusion of Participants in Choreographies

Maurizio Gabbrielli*, Saverio Giallorenzo, Ivan Lanese, Jacopo Mauro

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review


In Choreographic Programming, a choreography specifies in a single artefact the expected behaviour of all the participants in a distributed system. The choreography is used to synthesise correct-by-construction programs for each participant. In previous work, we defined Dynamic Choreographies to support the update of distributed systems at runtime. In this work, we extend Dynamic Choreographies to include new participants at runtime, capturing those use cases where the system might be updated to interact with new, unforeseen stakeholders. We formalise our extension, prove its correctness, and present an implementation in the AIOCJ choreographic framework.

Original languageEnglish
Title of host publicationThe Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy : Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday
EditorsMário S. Alvim, Kostas Chatzikokolakis, Carlos Olarte, Frank Valencia
PublisherSpringer VS
Publication date2019
ISBN (Print)978-3-030-31174-2
Publication statusPublished - 2019
SeriesLecture Notes in Computer Science


  • Adaptation of distributed systems
  • Choreographic programming
  • Dynamic inclusion of new software components

Cite this