Abstract
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.
Research partially supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No 778233.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
Annotated DIOC constructs are useful in the definition of the projection and the related proofs to avoid interference between different constructs.
- 3.
A compositional formalisation of function would require to check freshness at all the steps of the derivation of the transition, to avoid name clashes with roles which are not in the scope but only in the context. To simplify the presentation, here we assume that function has access to the set of roles of the whole DIOC .
- 4.
Note that in case the new roles cannot be instantiated, the adaptation rule is considered not applicable and the process of rule selection proceeds discarding this rule.
References
Montesi, F.: Kickstarting choreographic programming. In: Hildebrandt, T., Ravara, A., van der Werf, J.M., Weidlich, M. (eds.) WS-FM 2014-2015. LNCS, vol. 9421, pp. 3–10. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33612-1_1
Dalla Preda, M., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies: theory and implementation. Logical Methods Comput. Sci. 13(2) (2017)
Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: ASPLOS, pp. 329–339. ACM (2008)
Humble, J., Farley, D.: Continuous Delivery: Reliable Software Releases through Build, Test, and Deployment Automation. Pearson Education, London (2010)
Gabbrielli, M., Giallorenzo, S., Guidi, C., Mauro, J., Montesi, F.: Self-reconfiguring microservices. In: Ábrahám, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods. LNCS, vol. 9660, pp. 194–210. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30734-3_14
Bravetti, M., Giallorenzo, S., Mauro, J., Talevi, I., Zavattaro, G.: Optimal and automated deployment for microservices. In: Hähnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 351–368. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_21
AIOCJ website. http://www.cs.unibo.it/projects/jolie/aiocj.html
Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier Science Inc., New York (2001)
Montesi, F., Guidi, C., Zavattaro, G.: Service-oriented programming with Jolie. In: Bouguettaya, A., Sheng, Q., Daniel, F. (eds.) Web Services Foundations, pp. 81–107. Springer, New York (2014). https://doi.org/10.1007/978-1-4614-7518-7_4
Dragoni, N., et al.: Microservices: yesterday, today, and tomorrow. Present and Ulterior Software Engineering, pp. 195–216. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67425-4_12
Giallorenzo, S., Lanese, I., Russo, D.: ChIP: a choreographic integration process. In: Panetto, H., Debruyne, C., Proper, H., Ardagna, C., Roman, D., Meersman, R. (eds.) OTM 2018. Lecture Notes in Computer Science, vol. 11230, pp. 22–40. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02671-4_2
Giallorenzo, S., Lanese, I., Mauro, J., Gabbrielli, M.: Programming adaptive microservice applications: an AIOCJ tutorial. In: Behavioural Types: from Theory to Tools, pp. 147–167. River Publishers (2017)
Bucchiarone, A., Marconi, A., Pistore, M., Raik, H.: Dynamic adaptation of fragment-based and context-aware business processes. In: ICWS, pp. 33–41. IEEE (2012)
Chen, W.-K., Hiltunen, M.A., Schlichting, R.D.: Constructing adaptive software in distributed systems. ICDCS. LNCS, vol. 6084, pp. 635–643. Springer, Heidelberg (2001). https://doi.org/10.1109/ICDSC.2001.918994
Ghezzi, C., Pradella, M., Salvaneschi, G.: An evaluation of the adaptation capabilities in programming languages. In: SEAMS, pp. 50–59. ACM (2011)
Lanese, I., Bucchiarone, A., Montesi, F.: A framework for rule-based dynamic adaptation. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010. LNCS, vol. 6084, pp. 284–300. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15640-3_19
Zhang, J., Goldsby, H., Cheng, B.H.C.: Modular verification of dynamically adaptive systems. In: AOSD, pp. 161–172. ACM (2009)
Leite, L.A.F., et al.: A systematic literature review of service choreography adaptation. SOCA 7(3), 199–216 (2013)
Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8 (2012)
Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: POPL, pp. 263–274. ACM (2013)
Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party session. Logical Methods Comput. Sci. 8(1) (2012)
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273–284. ACM (2008)
Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: POPL, pp. 191–202. ACM (2012)
Lanese, I., Guidi, C., Montesi, F., Zavattaro, G.: Bridging the gap between interaction- and process-oriented choreographies. In: SEFM, pp. 323–332. IEEE (2008)
Bravetti, M., Zavattaro, G.: Towards a unifying theory for choreography conformance and contract compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34–50. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77351-1_4
Bergstra, J.A., Klint, P.: The discrete time TOOLBUS - a software coordination architecture. Sci. Comput. Program. 31(2–3), 205–229 (1998)
Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Self-adaptive multiparty sessions. SOCA 9(3–4), 249–268 (2015)
Di Giusto, C., Pérez, J.A.: Event-based run-time adaptation in communication-centric systems. Formal Asp. Comput. 28(4), 531–566 (2016)
Anderson, G., Rathke, J.: Dynamic software update for message passing programs. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 207–222. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35182-2_15
Montesi, F., Yoshida, N.: Compositional choreographies. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 425–439. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40184-8_30
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J. (2019). Guess Who’s Coming: Runtime Inclusion of Participants in Choreographies. In: Alvim, M., Chatzikokolakis, K., Olarte, C., Valencia, F. (eds) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. Lecture Notes in Computer Science(), vol 11760. Springer, Cham. https://doi.org/10.1007/978-3-030-31175-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-31175-9_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-31174-2
Online ISBN: 978-3-030-31175-9
eBook Packages: Computer ScienceComputer Science (R0)