{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T21:15:18Z","timestamp":1783545318300,"version":"3.55.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262196","type":"print"},{"value":"9783032262202","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Distributed runtime verification (DRV) addresses the problem of checking the correctness of distributed systems during execution, coping with partial knowledge, dynamic topologies, and the absence of global time. These challenges are particularly prominent in proximity-based networks, such as those arising in IoT and Far Edge computing scenarios, where large numbers of devices interact through local communication. This tutorial presents an approach to DRV based on Aggregate Programming (AP), a paradigm for designing distributed collective systems via high-level abstractions over computational fields. We show how temporal and spatial properties (expressed in past-CTL and SLCS, respectively) can be systematically compiled into aggregate monitors grounded in the eXchange Calculus and executed using the FCPP C++ framework and simulator for AP. The tutorial combines conceptual foundations with practical guidance: participants learn how to specify spatio-temporal properties, generate corresponding monitors, and execute them in a 3D simulation environment. Examples are drawn from ongoing industrial collaborations and research projects, which we use to illustrate realistic monitoring scenarios and motivate open challenges for AP-based DRV.<\/jats:p>","DOI":"10.1007\/978-3-032-26220-2_26","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T13:21:03Z","timestamp":1779024063000},"page":"550-575","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Distributed Runtime Verification in\u00a0Proximity-Based Networks: A Tutorial on\u00a0the\u00a0Aggregate Programming Approach"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2319-0375","authenticated-orcid":false,"given":"Giorgio","family":"Audrito","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8109-1706","authenticated-orcid":false,"given":"Ferruccio","family":"Damiani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2114-7435","authenticated-orcid":false,"given":"Giordano","family":"Scarso","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1031-6936","authenticated-orcid":false,"given":"Volker","family":"Stolz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4276-7213","authenticated-orcid":false,"given":"Gianluca","family":"Torta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"26_CR1","doi-asserted-by":"publisher","unstructured":"Aguzzi, G., Audrito, G., Viroli, M.: Optimising aggregate monitors for spatial logic of closure spaces properties. In: Proceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution, pp. 25\u201331. VORTEX 2024. ACM (2024). https:\/\/doi.org\/10.1145\/3679008.3685544","DOI":"10.1145\/3679008.3685544"},{"key":"26_CR2","doi-asserted-by":"publisher","unstructured":"Audrito, G.: FCPP: an efficient and extensible field calculus framework. In: Proceedings of the 1st International Conference on Autonomic Computing and Self-Organizing Systems, ACSOS, pp. 153\u2013159. IEEE Computer Society (2020). https:\/\/doi.org\/10.1109\/ACSOS49614.2020.00037","DOI":"10.1109\/ACSOS49614.2020.00037"},{"key":"26_CR3","doi-asserted-by":"publisher","unstructured":"Audrito, G., Beal, J., Damiani, F., Viroli, M.: Space-time universality of field calculus. In: Coord. Models and Languages. LNCS, vol. 10852, pp. 1\u201320. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-92408-3_1","DOI":"10.1007\/978-3-319-92408-3_1"},{"key":"26_CR4","doi-asserted-by":"publisher","unstructured":"Audrito, G., Casadei, R., Damiani, F., Salvaneschi, G., Viroli, M.: Functional programming for distributed systems with XC. In: 36th European Conference on Object-Oriented Programming, ECOOP 2022. LIPIcs, vol.\u00a0222, pp. 20:1\u201320:28. Schloss Dagstuhl (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2022.20","DOI":"10.4230\/LIPIcs.ECOOP.2022.20"},{"key":"26_CR5","doi-asserted-by":"publisher","unstructured":"Audrito, G., Casadei, R., Damiani, F., Salvaneschi, G., Viroli, M.: The exchange calculus (XC): a functional programming language design for distributed collective systems. J. Syst. Softw. 210 (2024). https:\/\/doi.org\/10.1016\/J.JSS.2024.111976","DOI":"10.1016\/J.JSS.2024.111976"},{"key":"26_CR6","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2021.110908","volume":"175","author":"G Audrito","year":"2021","unstructured":"Audrito, G., Casadei, R., Damiani, F., Stolz, V., Viroli, M.: Adaptive distributed monitors of spatial properties for cyber-physical systems. J. Syst. Softw. 175, 110908 (2021). https:\/\/doi.org\/10.1016\/j.jss.2021.110908","journal-title":"J. Syst. Softw."},{"key":"26_CR7","doi-asserted-by":"publisher","unstructured":"Audrito, G., Casadei, R., Damiani, F., Viroli, M.: Computation against a neighbour: addressing large-scale distribution and adaptivity with functional programming and Scala. Log. Methods Comput. Sci. 19(1) (2023). https:\/\/doi.org\/10.46298\/lmcs-19(1:6)2023","DOI":"10.46298\/lmcs-19(1:6)2023"},{"key":"26_CR8","doi-asserted-by":"publisher","unstructured":"Audrito, G., Damiani, F., Rinaldi, S., Tagliabue, L.C., Testa, L., Torta, G.: Aggregate programming for customized building management and users preference implementation, pp. 147\u2013172. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-15160-6_7","DOI":"10.1007\/978-3-031-15160-6_7"},{"key":"26_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2022.111251","volume":"187","author":"G Audrito","year":"2022","unstructured":"Audrito, G., Damiani, F., Stolz, V., Torta, G., Viroli, M.: Distributed runtime verification by past-CTL and the field calculus. J. Syst. Softw. 187, 111251 (2022). https:\/\/doi.org\/10.1016\/j.jss.2022.111251","journal-title":"J. Syst. Softw."},{"key":"26_CR10","doi-asserted-by":"publisher","unstructured":"Audrito, G., Damiani, F., Torta, G.: Real-time guarantees for SLCS monitors in XC. In: VORTEX Proceedings of VORTEX 2024. pp. 32\u201337. ACM (2024). https:\/\/doi.org\/10.1145\/3679008.3685545","DOI":"10.1145\/3679008.3685545"},{"key":"26_CR11","doi-asserted-by":"publisher","unstructured":"Audrito, G., Rapetta, L., Torta, G.: Extensible 3d simulation of aggregated systems with FCPP. In: Coordination Models and Languages. LNCS, vol. 13271, pp. 55\u201371. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-08143-9_4","DOI":"10.1007\/978-3-031-08143-9_4"},{"issue":"3","key":"26_CR12","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1109\/TPDS.2022.3232633","volume":"34","author":"G Audrito","year":"2023","unstructured":"Audrito, G., Terraneo, F., Fornaciari, W.: FCPP+Miosix: scaling aggregate programming to embedded systems. IEEE Trans. Parallel Distributed Syst. 34(3), 869\u2013880 (2023). https:\/\/doi.org\/10.1109\/TPDS.2022.3232633","journal-title":"IEEE Trans. Parallel Distributed Syst."},{"key":"26_CR13","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2023.103026","volume":"231","author":"G Audrito","year":"2024","unstructured":"Audrito, G., Torta, G.: FCPP to aggregate them all. Sci. Comput. Program. 231, 103026 (2024). https:\/\/doi.org\/10.1016\/J.SCICO.2023.103026","journal-title":"Sci. Comput. Program."},{"key":"26_CR14","doi-asserted-by":"publisher","unstructured":"Audrito, G., Viroli, M., Damiani, F., Pianini, D., Beal, J.: A higher-order calculus of computational fields. ACM Trans. Comput. Logic 20(1), 5:1\u20135:55 (2019). https:\/\/doi.org\/10.1145\/3285956","DOI":"10.1145\/3285956"},{"key":"26_CR15","doi-asserted-by":"publisher","unstructured":"Beal, J., Pianini, D., Viroli, M.: Aggregate programming for the Internet of Things. IEEE Comput. 48(9) (2015). https:\/\/doi.org\/10.1109\/MC.2015.261","DOI":"10.1109\/MC.2015.261"},{"key":"26_CR16","doi-asserted-by":"publisher","unstructured":"Casadei, R., Aguzzi, G., Pianini, D., Viroli, M.: Programming (and learning) self-adaptive & self-organising behaviour with ScaFi: for swarms, edge-cloud ecosystems, and more. In: IEEE International Conference on Autonomic Computing and Self-organizing Systems, ACSOS 2023, Toronto, Canada, September 25-29, 2023. pp. 33\u201334. IEEE (2023). https:\/\/doi.org\/10.1109\/ACSOS-C58168.2023.00032","DOI":"10.1109\/ACSOS-C58168.2023.00032"},{"issue":"20","key":"26_CR17","doi-asserted-by":"publisher","first-page":"20136","DOI":"10.1109\/JIOT.2022.3172470","volume":"9","author":"R Casadei","year":"2022","unstructured":"Casadei, R., Fortino, G., Pianini, D., Placuzzi, A., Savaglio, C., Viroli, M.: A methodology and simulation-based toolchain for estimating deployment performance of smart collective services at the edge. IEEE Internet Things J. 9(20), 20136\u201320148 (2022). https:\/\/doi.org\/10.1109\/JIOT.2022.3172470","journal-title":"IEEE Internet Things J."},{"key":"26_CR18","doi-asserted-by":"publisher","unstructured":"Casadei, R., Viroli, M.: Towards aggregate programming in Scala. In: 1st PMLDC Workshop, New York, NY, USA, pp. 5:1\u20135:7. ACM (2016). https:\/\/doi.org\/10.1145\/2957319.2957372","DOI":"10.1145\/2957319.2957372"},{"key":"26_CR19","doi-asserted-by":"publisher","DOI":"10.1016\/j.softx.2022.101248","volume":"20","author":"R Casadei","year":"2022","unstructured":"Casadei, R., Viroli, M., Aguzzi, G., Pianini, D.: SCAFI: a scala DSL and toolkit for aggregate programming. SoftwareX 20, 101248 (2022). https:\/\/doi.org\/10.1016\/j.softx.2022.101248","journal-title":"SoftwareX"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-662-44602-7_18","volume-title":"Theoretical Computer Science","author":"V Ciancia","year":"2014","unstructured":"Ciancia, V., Latella, D., Loreti, M., Massink, M.: Specifying and verifying properties of space. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 222\u2013235. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44602-7_18"},{"key":"26_CR21","doi-asserted-by":"publisher","unstructured":"Cortecchia, A.: Multiplatform self-organizing systems through a kotlin-mp implementation of aggregate computing. In: 2024 IEEE International Conference on Autonomic Computing and Self-organizing Systems Companion (ACSOS-C), pp. 155\u2013157 (2024). https:\/\/doi.org\/10.1109\/ACSOS-C63493.2024.00048","DOI":"10.1109\/ACSOS-C63493.2024.00048"},{"issue":"4","key":"26_CR22","doi-asserted-by":"publisher","first-page":"4092","DOI":"10.1109\/TKDE.2022.3142856","volume":"35","author":"S Dustdar","year":"2023","unstructured":"Dustdar, S., Pujol, V.C., Donta, P.K.: On distributed computing continuum systems. IEEE Trans. Knowl. Data Eng. 35(4), 4092\u20134105 (2023). https:\/\/doi.org\/10.1109\/TKDE.2022.3142856","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"26_CR23","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"},{"key":"26_CR24","doi-asserted-by":"publisher","unstructured":"Gigante, N., Montanari, A., Reynolds, M.: A one-pass tree-shaped tableau for ltl+past. In: LPAR-21. EPiC Series in Computing, vol.\u00a046, pp. 456\u2013473. EasyChair (2017). https:\/\/doi.org\/10.29007\/3HB9","DOI":"10.29007\/3HB9"},{"issue":"7","key":"26_CR25","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978). https:\/\/doi.org\/10.1145\/359545.359563","journal-title":"Commun. ACM"},{"issue":"5","key":"26_CR26","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293\u2013303 (2009). https:\/\/doi.org\/10.1016\/j.jlap.2008.08.004","journal-title":"J. Logic Algebraic Program."},{"key":"26_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-39173-8_6","volume-title":"Engineering Societies in the Agents World III","author":"M Mamei","year":"2003","unstructured":"Mamei, M., Zambonelli, F., Leonardi, L.: Co-Fields: towards a unifying approach to the engineering of swarm intelligent systems. In: Petta, P., Tolksdorf, R., Zambonelli, F. (eds.) ESAW 2002. LNCS (LNAI), vol. 2577, pp. 68\u201381. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-39173-8_6"},{"key":"26_CR28","doi-asserted-by":"publisher","unstructured":"Nitti, L., et al.: Drone-swarm based surveillance system for autonomous machine safety functionality. In: Precision Agriculture 2025. LNCS, vol.\u00a02577, pp. 492\u2013598. Springer, Cham (2002). https:\/\/doi.org\/10.1163\/9789004725232_077","DOI":"10.1163\/9789004725232_077"},{"key":"26_CR29","doi-asserted-by":"publisher","unstructured":"Saint-Martin, L., et al.: Study on the economic potential of far edge computing in the future smart Internet of Things. Final study report, European Commission: Decision Etudes & Conseil, Directorate-General for Communications Networks, Content and Technology (2023). https:\/\/doi.org\/10.2759\/05608","DOI":"10.2759\/05608"},{"key":"26_CR30","unstructured":"Santer REPLY SpA: The RoboNG project (2023). https:\/\/ecs-nodes.eu\/en\/1-aerospace-and-sustainable-mobility\/progetti-imprese\/robong. Accessed 9 Feb 2026"},{"key":"26_CR31","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2022.101658","volume":"85","author":"L Testa","year":"2022","unstructured":"Testa, L., Audrito, G., Damiani, F., Torta, G.: Aggregate processes as distributed adaptive services for the industrial internet of things. Pervasive Mob. Comput. 85, 101658 (2022). https:\/\/doi.org\/10.1016\/j.pmcj.2022.101658","journal-title":"Pervasive Mob. Comput."},{"key":"26_CR32","unstructured":"University of Bologna: ScaFi Aggregate Programming Toolkit (2018). https:\/\/scafi.github.io\/. Accessed 9 Feb 2026"},{"key":"26_CR33","unstructured":"University of Bologna: Collektive (2024). https:\/\/collektive.github.io. Accessed 9 Feb 2026"},{"key":"26_CR34","unstructured":"University of Turin: The RoboAPP project (2024). https:\/\/ai4future.unito.it\/roboapp\/ and https:\/\/ecs-nodes.eu\/en\/1-aerospace-and-sustainable-mobility\/progetti-accademici\/roboapp. Accessed 9 Feb 2026"},{"key":"26_CR35","unstructured":"University of Turin: FCPP (2021). https:\/\/fcpp.github.io\/. Accessed 9 Feb 2026"},{"key":"26_CR36","doi-asserted-by":"publisher","unstructured":"Viroli, M., Audrito, G., Beal, J., Damiani, F., Pianini, D.: Engineering resilient collective adaptive systems by self-stabilisation. ACM Trans. Model. Comput. Simul. 28(2), 16:1\u201316:28 (2018). https:\/\/doi.org\/10.1145\/3177774","DOI":"10.1145\/3177774"},{"key":"26_CR37","doi-asserted-by":"publisher","unstructured":"Viroli, M., Beal, J., Damiani, F., Audrito, G., Casadei, R., Pianini, D.: From distributed coordination to field calculus and aggregate computing. J. Log. Algebraic Methods Program. 109 (2019). https:\/\/doi.org\/10.1016\/j.jlamp.2019.100486","DOI":"10.1016\/j.jlamp.2019.100486"},{"issue":"6","key":"26_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-024-40231-1","volume":"18","author":"L Wang","year":"2024","unstructured":"Wang, L., et al.: A survey on large language model based autonomous agents. Front. Comp. Sci. 18(6), 186345 (2024). https:\/\/doi.org\/10.1007\/s11704-024-40231-1","journal-title":"Front. Comp. Sci."},{"key":"26_CR39","doi-asserted-by":"publisher","unstructured":"Winskel, G.: Event structure semantics for CCS and related languages. In: Nielsen, M., Schmidt, E.M. (eds.) Automata, Languages and Programming, 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings. LNCS, vol.\u00a0140, pp. 561\u2013576. Springer (1982). https:\/\/doi.org\/10.1007\/BFB0012800","DOI":"10.1007\/BFB0012800"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26220-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T20:29:05Z","timestamp":1783542545000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26220-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262196","9783032262202"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26220-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}