{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:35:49Z","timestamp":1762299349819,"version":"3.40.3"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030473600"},{"type":"electronic","value":"9783030473617"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,5,12]],"date-time":"2020-05-12T00:00:00Z","timestamp":1589241600000},"content-version":"vor","delay-in-days":132,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Distributed programs are hard to get right because they are required to be open, scalable, long-running, and dependable. In particular, the recent approaches to distributed software based on (micro-) services, where different services are developed independently by disparate teams, exacerbate the problem. Services are meant to be composed together and run in open contexts where unpredictable behaviours can emerge. This makes it necessary to adopt suitable strategies for monitoring the execution and incorporate recovery and adaptation mechanisms so to make distributed programs more flexible and robust. The typical approach that is currently adopted is to embed such mechanisms within the program logic. This makes it hard to extract, compare and debug. We propose an approach that employs formal abstractions for specifying failure recovery and adaptation strategies. Although implementation agnostic, these abstractions would be amenable to algorithmic synthesis of code, monitoring, and tests. We consider message-passing programs (a la Erlang, Go, or MPI) that are gaining momentum both in academia and in industry. We first propose a model which abstracts away from three aspects: the definition of formal behavioural models encompassing failures; the specification of the relevant properties of adaptation and recovery strategy; and the automatic generation of monitoring, recovery, and adaptation logic in target languages of interest. To show the efficacy of our model, we give an instance of it by introducing <jats:italic>reversible choreographies<\/jats:italic> to express the normal forward behaviour of the system and the condition under which adaptation has to take place. Then we show how it is possible to derive Erlang code directly from the global specification.<\/jats:p>","DOI":"10.1007\/978-3-030-47361-7_6","type":"book-chapter","created":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T15:10:54Z","timestamp":1589382654000},"page":"128-150","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Towards Choreographic-Based Monitoring"],"prefix":"10.1007","author":[{"given":"Adrian","family":"Francalanza","sequence":"first","affiliation":[]},{"given":"Claudio Antares","family":"Mezzina","sequence":"additional","affiliation":[]},{"given":"Emilio","family":"Tuosto","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,5,12]]},"reference":[{"key":"6_CR1","unstructured":"Erlang run-time system application, reference manual version 9.2 (2017)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. 3(POPL), 52:1\u201352:29 (2019)","DOI":"10.1145\/3290365"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-030-21485-2_4","volume-title":"Models, Languages, and Tools for Concurrent and Distributed Programming","author":"L Aceto","year":"2019","unstructured":"Aceto, L., Achilleos, A., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A., Lehtinen, K.: Testing equivalence vs. runtime monitoring. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665, pp. 28\u201344. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-21485-2_4"},{"key":"6_CR4","unstructured":"Aceto, L., Cassar, I., Francalanza, A., Ing\u00f3lfsd\u00f3ttir, A.: On runtime enforcement via suppressions. In: 29th International Conference on Concurrency Theory, CONCUR 2018, Beijing, China, 4\u20137 September 2018. LIPIcs, vol. 118, pp. 34:1\u201334:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)"},{"key":"6_CR5","series-title":"MIT Press Series in Artificial Intelligence","volume-title":"ACTORS - A Model of Concurrent Computation in Distributed Systems","author":"GA Agha","year":"1990","unstructured":"Agha, G.A.: ACTORS - A Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence. MIT Press, Cambridge (1990)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-319-46982-9_31","volume-title":"Runtime Verification","author":"DP Attard","year":"2016","unstructured":"Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 473\u2013481. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_31"},{"issue":"3","key":"6_CR7","first-page":"425","volume":"85","author":"D Basile","year":"2016","unstructured":"Basile, D., Degano, P., Ferrari, G.-L., Tuosto, E.: Relating two automata-based models of orchestration and choreography. JLAMP 85(3), 425\u2013446 (2016)","journal-title":"JLAMP"},{"issue":"2","key":"6_CR8","first-page":"1","volume":"11","author":"G Bernardi","year":"2015","unstructured":"Bernardi, G., Hennessy, M.: Mutually testing processes. LMCS 11(2), 1\u201323 (2015)","journal-title":"LMCS"},{"issue":"2","key":"6_CR9","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-23820-3_3","volume-title":"Runtime Verification","author":"I Cassar","year":"2015","unstructured":"Cassar, I., Francalanza, A.: Runtime adaptation for actor systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 38\u201354. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23820-3_3"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-33693-0_12","volume-title":"Integrated Formal Methods","author":"I Cassar","year":"2016","unstructured":"Cassar, I., Francalanza, A.: On implementing a monitor-oriented programming framework for actor systems. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 176\u2013192. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_12"},{"key":"6_CR12","unstructured":"Cassar, I., Francalanza, A., Attard, D.P., Aceto, L., Ing\u00f3lfsd\u00f3ttir, A.: A suite of monitoring tools for Erlang. In: Reger, G., Havelund, K. (eds.) RV-CuBES 2017. An International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools. Kalpa Publications in Computing, vol. 3, pp. 41\u201347. EasyChair (2017)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Cassar, I., Francalanza, A., Mezzina, C.A., Tuosto, E.: Reliability and fault-tolerance by choreographic design. In: PrePost@iFM. EPTCS, vol. 254 (2017)","DOI":"10.4204\/EPTCS.254.6"},{"issue":"5","key":"6_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1538917.1538920","volume":"31","author":"G Castagna","year":"2009","unstructured":"Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Trans. Program. Lang. Syst. 31(5), 1\u201361 (2009)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-17685-2_2","volume-title":"Central European Functional Programming School","author":"F Cesarini","year":"2010","unstructured":"Cesarini, F., Thompson, S.: Erlang behaviours: programming with process design patterns. In: Horv\u00e1th, Z., Plasmeijer, R., Zs\u00f3k, V. (eds.) CEFP 2009. LNCS, vol. 6299, pp. 19\u201341. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17685-2_2"},{"key":"6_CR16","unstructured":"Chen, F., Jin, D., Meredith, P., Ro\u015fu, G.: Monitoring oriented programming - a project overview. In: Proceedings of the Fourth International Conference on Intelligent Computing and Information Systems (ICICIS 2009), pp. 72\u201377. ACM (2009)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-030-18506-0_2","volume-title":"Trends in Functional Programming","author":"F de Vries","year":"2019","unstructured":"de Vries, F., P\u00e9rez, J.A.: Reversible session-based concurrency in Haskell. In: Pa\u0142ka, M., Myreen, M. (eds.) TFP 2018. LNCS, vol. 11457, pp. 20\u201345. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-18506-0_2"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-28869-2_10","volume-title":"Programming Languages and Systems","author":"P-M Deni\u00e9lou","year":"2012","unstructured":"Deni\u00e9lou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194\u2013213. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_10"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Field, J., Varela, C.A.: Transactors: a programming model for maintaining globally consistent distributed state in unreliable environments. In: POPL 2005. ACM (2005)","DOI":"10.1145\/1040305.1040322"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-662-49630-5_9","volume-title":"Foundations of Software Science and Computation Structures","author":"A Francalanza","year":"2016","unstructured":"Francalanza, A.: A theory of monitors - (extended abstract). In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 145\u2013161. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_9"},{"key":"6_CR21","unstructured":"Francalanza, A.: Consistently-detecting monitors. In: 28th International Conference on Concurrency Theory, CONCUR 2017, 5\u20138 September 2017. LIPIcs, vol. 85, pp. 8:1\u20138:19. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-017-0273-z","volume":"51","author":"A Francalanza","year":"2017","unstructured":"Francalanza, A., Aceto, L., Ingolfsdottir, A.: Monitorability for the Hennessy-Milner logic with recursion. Formal Methods Syst. Des. 51, 1\u201330 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0273-z","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-319-93767-0_6","volume-title":"Distributed Applications and Interoperable Systems","author":"A Francalanza","year":"2018","unstructured":"Francalanza, A., Mezzina, C.A., Tuosto, E.: Reversible choreographies via monitoring in Erlang. In: Bonomi, S., Rivi\u00e8re, E. (eds.) DAIS 2018. LNCS, vol. 10853, pp. 75\u201392. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-93767-0_6"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-75632-5_6","volume-title":"Lectures on Runtime Verification","author":"A Francalanza","year":"2018","unstructured":"Francalanza, A., P\u00e9rez, J.A., S\u00e1nchez, C.: Runtime verification for decentralised and distributed systems. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 176\u2013210. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_6"},{"issue":"3","key":"6_CR25","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/s10703-014-0217-9","volume":"46","author":"A Francalanza","year":"2015","unstructured":"Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Methods Syst. Des. (FMSD) 46(3), 226\u2013261 (2015). https:\/\/doi.org\/10.1007\/s10703-014-0217-9","journal-title":"Formal Methods Syst. Des. (FMSD)"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-54804-8_26","volume-title":"Fundamental Approaches to Software Engineering","author":"E Giachino","year":"2014","unstructured":"Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 370\u2013384. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54804-8_26"},{"key":"6_CR27","unstructured":"Gray, J.: Why do computers stop and what can be done about it? In: SRDS. IEEE (1986)"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Guanciale, R., Tuosto, E.: An abstract semantics of the global view of choreographies. In: ICE 2016, Heraklion, Greece, pp. 67\u201382 (2016)","DOI":"10.4204\/EPTCS.223.5"},{"key":"6_CR29","unstructured":"Hewitt, C., Bishop, P., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: IJCAI. Morgan Kaufmann Publishers Inc. (1973)"},{"key":"6_CR30","unstructured":"Kavantzas, N., Burdett, D., Ritzinger, G., Fletcher, T., Lafon, Y.: Web services choreography description language version 1.0 (2004). http:\/\/www.w3.org\/TR\/2004\/WD-ws-cdl-10-20041217"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-36315-3_19","volume-title":"Reversible Computation","author":"I Lanese","year":"2013","unstructured":"Lanese, I., Mezzina, C.A., Stefani, J.-B.: Controlled reversibility and compensations. In: Gl\u00fcck, R., Yokoyama, T. (eds.) RC 2012. LNCS, vol. 7581, pp. 233\u2013240. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36315-3_19"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-90686-7_16","volume-title":"Functional and Logic Programming","author":"I Lanese","year":"2018","unstructured":"Lanese, I., Nishida, N., Palacios, A., Vidal, G.: CauDEr: a causal-consistent reversible debugger for Erlang. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 247\u2013263. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-90686-7_16"},{"key":"6_CR33","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.jlamp.2018.06.004","volume":"100","author":"I Lanese","year":"2018","unstructured":"Lanese, I., Nishida, N., Palacios, A., Vidal, G.: A theory of reversibility for Erlang. J. Log. Algebraic Methods Program. 100, 71\u201397 (2018)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Lange, J., Tuosto, E., Yoshida, N.: From communicating machines to graphical choreographies. In: POPL, pp. 221\u2013232 (2015)","DOI":"10.1145\/2775051.2676964"},{"key":"6_CR35","first-page":"249","volume":"14","author":"PO Meredith","year":"2011","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Ro\u015fu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tech. Technol. Transf. 14, 249\u2013289 (2011)","journal-title":"Int. J. Softw. Tech. Technol. Transf."},{"issue":"3","key":"6_CR36","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/MS.2014.58","volume":"31","author":"M Meyer","year":"2014","unstructured":"Meyer, M.: Continuous integration and its tools. IEEE Softw. 31(3), 14\u201316 (2014)","journal-title":"IEEE Softw."},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Mezzina, C.A., P\u00e9rez, J.A.: Causally consistent reversible choreographies: a monitors-as-memories approach. In: PPDP (2017)","DOI":"10.1145\/3131851.3131864"},{"key":"6_CR38","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.jlamp.2017.03.003","volume":"90","author":"CA Mezzina","year":"2017","unstructured":"Mezzina, C.A., P\u00e9rez, J.A.: Reversibility in session-based concurrency: a fresh look. J. Log. Algebr. Meth. Program. 90, 2\u201330 (2017)","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"6_CR39","unstructured":"Mezzina, C.A., Tuosto, E.: Choreographies for automatic recovery. CoRR, abs\/1705.09525 (2017)"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: CC. ACM (2017)","DOI":"10.1145\/3033019.3033031"},{"key":"6_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-642-36315-3_18","volume-title":"Reversible Computation","author":"I Phillips","year":"2013","unstructured":"Phillips, I., Ulidowski, I., Yuen, S.: A reversible process calculus and the modelling of the ERK signalling pathway. In: Gl\u00fcck, R., Yokoyama, T. (eds.) RC 2012. LNCS, vol. 7581, pp. 218\u2013232. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36315-3_18"},{"key":"6_CR42","volume-title":"Software Reliability Handbook","author":"P Rook","year":"1990","unstructured":"Rook, P.: Software Reliability Handbook. Elsevier Science Inc., New York (1990)"},{"issue":"1","key":"6_CR43","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"6_CR44","unstructured":"Thomas, D.: Programming Elixir: Functional, Concurrent, Pragmatic, Fun, 1st edn. Pragmatic Bookshelf (2014)"},{"key":"6_CR45","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlamp.2017.11.002","volume":"95","author":"E Tuosto","year":"2018","unstructured":"Tuosto, E., Guanciale, R.: Semantics of global view of choreographies. J. Log. Algebr. Meth. Program. 95, 17\u201340 (2018)","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"6_CR46","unstructured":"Wyatt, D.: Akka Concurrency. Artima Incorporation, USA (2013)"}],"container-title":["Lecture Notes in Computer Science","Reversible Computation: Extending Horizons of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-47361-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,3]],"date-time":"2024-07-03T10:04:32Z","timestamp":1720001072000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-47361-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030473600","9783030473617"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-47361-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"12 May 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}