Abstract
This volume contains the proceedings of the Colloquium in honor of Rocco De Nicola’s 70th birthday, held jointly with the ISOLA 2024’s track on REoCAS (Rigorous Engineering of Collective Adaptive Systems). Rocco De Nicola has significantly contributed to collective adaptive systems through novel approaches for their formal specification, analysis, and verification. The Colloquium features one homage paper and 23 contributions from invited authors who reflected upon these developments within the context of Rocco’s much broader legacy in concurrency theory, distributed systems, domain-specific languages, service-oriented computing, and formal methods, exploring his recent contributions to cybersecurity.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abd Alrahman, Y., De Nicola, R., Loreti, M.: A calculus for collective-adaptive systems and its behavioural theory. Inf. Comput. 268, 104457 (2019)
Aceto, L., Gorla, D., Lybech, S.: Preventing out-of-gas exceptions by typing. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 409–426. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_25
Andrade, L., et al.: AGILE: software architecture for mobility. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2002. LNCS, vol. 2755, pp. 1–33. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-40020-2_1
Barbanera, F., Dezani-Ciancaglini, M.: Asynchronous multiparty sessions with internal delegation. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 322–339. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_20
Bartocci, E.: The ProbInG project: computing automatically invariants for probabilistic loops. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 152–167. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_10
Belzner, L., De Nicola, R., Vandin, A., Wirsing, M.: Reasoning (on) service component ensembles in rewriting logic. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 188–211. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54624-2_10
Bettini, L., Ferrari, G.-L., Loreti, M., Pugliese, R., Tiezzi, F., Tuosto, E.: Klaim in the making. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 27–49. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_3
Bistarelli, S., Santini,: Local spaces in soft concurrent constraint programming oriented to security. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 373–391. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_23
Boreale, M., et al.: SCC: a service centered calculus. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 38–57. Springer, Heidelberg (2006). https://doi.org/10.1007/11841197_3
Boreale, M., Bruni, R., De Nicola, R., Loreti, M.: Sessions and pipelines for structured service programming. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 19–38. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68863-1_3
Boreale, M., Collodi, L.: Language equivalence from nondeterministic to weighted automata - and back. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 75–93. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_6
Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.): Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21485-2
Boreale, M., De Nicola, R., Pugliese, R.: Proof techniques for cryptographic processes. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, 2–5 July 1999, pp. 157–166. IEEE Computer Society (1999)
Bortolussi, L., et al.: CARMA: collective adaptive resource-sharing markovian agents. In: Bertrand, N., Tribastone, M. (eds.) Proceedings Thirteenth Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2015, London, UK, 11–12 April 2015, vol. 194 of EPTCS, pp. 16–31 (2015)
Bottoni, P., Labella, A., Perelli, G.: Strategies in spatio-temporal logics for multi-agent systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 287–305. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_18
Bruni, R.: A process algebraic view of in/out prisoners: from TAPAs to CAAL. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 94–110. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_7
Bureš, T., et al.: A life cycle for the development of autonomic systems: the e-mobility showcase. In: SASO Workshops 2013, pp. 71–76 (2013)
Busch, D., Smyth, S., Tegeler, T., Steffen, B.: Code-centric code generation. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 340–355. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_21
Caires, L., De Nicola, R., Pugliese, R., Vasconcelos, V.T., Zavattaro, G.: Core calculi for service-oriented computing. In: Wirsing, M., Hölzl, M. (eds.) Rigorous Software Engineering for Service-Oriented Systems. LNCS, vol. 6582, pp. 153–188. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20401-2_8
Caldarelli, G., De Nicola, R., Petrocchi, M., Pratelli, M., Saracco, F.: Flow of online misinformation during the peak of the COVID-19 pandemic in italy. EPJ Data Sci. 10(1), 34 (2021)
Calzolai, F., De Nicola, R., Loreti, M., Tiezzi, F.: TAPAs: a tool for the analysis of process algebras. In: Jensen, K., van der Aalst, W.M.P., Billington, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency I. LNCS, vol. 5100, pp. 54–70. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89287-8_4
Cao, Y., Gillespie, D.T., Petzold, L.R.: Efficient step size selection for the tau-leaping simulation method. J. Chem. Phys. 124(4), 044109 (2006)
Casaluce, R., Burattin, A., Chiaromonte, F., Lluch-Lafuente, A., Vandin, A.: White-box validation of quantitative product lines by statistical model checking and process mining. J. Syst. Softw. 210, 111983 (2024)
Casaluce, R., Tschaikowski, M., Vandin, A.: White-box validation of collective adaptive systems by statistical model checking and process mining. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 204–222. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_13
Ceragioli, L., Gadducci, F., Lomurno, G., Tedeschi, G.: Testing quantum processes. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 132–151. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_9
Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F.: A formal approach to modeling and verification of business process collaborations. Sci. Comput. Program. 166, 35–70 (2018)
Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., Vandin, A.: Bprove: a formal verification framework for business process models. In: Rosu, G., Penta, M.D., Nguyen, T.N. (eds.) Proceedings of 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, pp. 217–228. IEEE Computer Society (2017)
Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., Vandin, A. Bprove: tool support for business process verification. In: Rosu, G., Penta, M.D., Nguyen, T.N. (eds.) Proceedings of 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, pp. 937–942. IEEE Computer Society, 2017
Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., Vandin, A.: A formal approach for the analysis of BPMN collaboration models. J. Syst. Softw. 180, 111007 (2021)
Corradini,F., Fornari, F., Re, B., Rossi, L., Polini, A., Tiezzi, F., Vandin, A.: Formal approaches for modeling and analysis of business process collaborations. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 50–61. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_4
Corradini, F., Muzi, C., Re, B., Rossi, L., Tiezzi, F.: BPMN 2.0 OR-join semantics: global and local characterisation. Inf. Syst. 105, 101934 (2022)
Corradini, F., Polini, A., Re, B., Tiezzi, F.: An operational semantics of BPMN collaboration. In: Braga, C., Ölveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 161–180. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-28934-2_9
Costa, G., et al.: Systems security modeling and analysis at IMT Lucca. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 13–26. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_2
De Nicola, R.: Extensional equivalences for transition systems. Acta Informatica 24(2), 211–237 (1987)
De Nicola, R., Di Stefano, L., Inverso, O., Valiani, S.: Modelling flocks of birds and colonies of ants from the bottom up. JSTTT 25(5), 675–691 (2023)
De Nicola, R., Ferrari, G., Pugliese, R., Tiezzi, F.: A formal approach to the engineering of domain-specific distributed systems. J. Log. Algebraic Methods Program. 111, 100511 (2020)
De Nicola, R., Ferrari, G.-L., Pugliese, R.: KLAIM: a kernel language for agents interaction and mobility. IEEE Trans. Softw. Eng. 24(5), 315–330 (1998)
De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoret. Comput. Sci. 34(1), 83–133 (1984)
De Nicola, R., Katoen, J., Latella, D., Massink, M.: Towards a logic for performance and mobility. In: Cerone, A., Wiklicky, H. (eds.) Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, QAPL 2005, Edinburgh, UK, 2–3 April 2005, vol. 153 of Electronic Notes in Theoretical Computer Science, pp. 161–175. Elsevier (2005)
De Nicola, R., Loreti, M.: A modal logic for mobile agents. ACM Trans. Comput. Logic (TOCL) 5(1), 79–128 (2004)
Nicola, R. D., Loreti, M., Pugliese, R., Tiezzi, F.: A formal approach to autonomic systems programming: the SCEL language. ACM Trans. Auton. Adapt. Syst. (TAAS) 9(2), 7:1–7:29 (2014)
De Nicola, R., Melgratti, H.: Multiparty testing preorders. Logical Methods Comput. Sci. 19 (2023)
De Nicola, R., Petrocchi, M., Pratelli, M.: On the efficacy of old features for the detection of new bots. Inf. Process. Manag. 58(6), 102685 (2021)
De Palma, G., Giallorenzo, S., Mauro, J., Trentin, M., Zavattaro, G.: Function-as-a-service allocation policies made formal. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 306–321. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_19
De Palma, G., Giallorenzo, S., Mauro, J., Zavattaro, G.: Allocation priority policies for serverless function-execution scheduling optimisation. In: Kafeza, E., Benatallah, B., Martinelli, F., Hacid, H., Bouguettaya, A., Motahari, H. (eds.) ICSOC 2020. LNCS, vol. 12571, pp. 416–430. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-65310-1_29
De Sanctis, M., Inverardi, P.: Engineering ethical-aware collective adaptive systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 238–252. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_15
Di Stefano, L., Inverso, O.: Emerging synchrony in applauding audiences: formal analysis and specification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 253–270. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_16
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker and its implementation. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 230–234. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44829-2_16
Hajny, J., Ricci, S., Piesarskas, E., Levillain, O., Galletta, L., De Nicola, R.: Framework, tools and good practices for cybersecurity curricula. IEEE Access 9, 94723–94747 (2021)
Incerto, E., Trubiani, C.: Flocks of birds: a quantitative evaluation. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 271–286. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_17
Konsta, A.-M., Di Federico, G., Lluch Lafuente, A., Burattin, A.: Attack tree generation via process mining. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 356–372. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_22
Margaria, T., Steffen, B. (eds.): ISoLA 2014. LNCS, vol. 8802. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45234-9
Margaria, T., Steffen, B. (eds.): ISoLA 2014. LNCS, vol. 13703. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-031-19759-8
Montanari, U.: From tuscany to scotland and back. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds.) Models, Languages, and Tools for Concurrent and Distributed Programming. LNCS, vol. 11665, pp. 3–6. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-21485-2_1
Mousavi, M.R., Peters, K., Schmitt, A.: Towards a formal testing theory for quantum processes. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 111–131. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_8
Perini Brogi, C., Maggesi, M.: Analysing collective adaptive systems by proving theorems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 223–237. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_14
Randone, F., Bortolussi, L., Incerto, E., Tribastone, M.: Inference of probabilistic programs with moment-matching Gaussian mixtures. Proc. ACM Program. Lang. 8(POPL), 1882–1912 (2024)
Randone, F., Doz, R., Cairoli, F., Bortolussi, L.: Towards a probabilistic programming approach to analyse collective adaptive systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 168–185. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_11
Rubino, F., Bodei, C., Ferrari, G.-L.: Riding the data storms: specifying and analysing IoT security requirements with SURFING. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 392–408. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_24
Sangiorgi, D.: An abstract account of up-to techniques for inductive behavioural relations. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 62–74. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_5
Sebastio, S., Vandin, A.: Multivesta: statistical model checking for discrete event simulators. In: Horváth, A., Buchholz, P., Cortellessa, V., Muscariello, L., Squillante, M.S. (eds.) 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools ’13, Torino, Italy, 10–12 December 2013, pp. 310–315. ICST/ACM (2013)
Soderi, S., De Nicola, R.: 6G networks physical layer security using RGB visible light communications. IEEE Access 10, 5482–5496 (2022)
ter Beek, M.H., Fantechi, A., Gnesi, S., Lenzini, G., Petrocchi, M.: Can AI help with the formalization of railway cybersecurity requirements? In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, pp. 186–203. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-031-73709-1_12
Uriarte, R.B., De Nicola, R., Scoca, V., Tiezzi, F.: Defining and guaranteeing dynamic service levels in clouds. Future Gener. Comput. Syst. 99, 27–40 (2019)
Uriarte, R.B., Tiezzi, F., De Nicola, R.: SLAC: a formal service-level-agreement language for cloud computing. In: 7th IEEE/ACM International Conference on Utility and Cloud Computing, UCC 2014, pp. 419–426. IEEE Computer Society (2014)
Vandin, A., Giachini, D., Lamperti, F., Chiaromonte, F.: Automated and distributed statistical analysis of economic agent-based models. J. Econ. Dyn. Control 143, 104458 (2022)
Wirsing, M., et al.: Sensoria process calculi for service-oriented computing. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 30–50. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75336-0_3
Wirsing, M., De Nicola, R., Hölzl, M.M.: Rigorous engineering of autonomic ensembles – track introduction. In: [52], pp. 96–98 (2014)
Wirsing, M., De Nicola, R., Jähnichen, S.: Rigorous engineering of collective adaptive systems – introduction to the \(4^{\text{th}}\) track edition. In: [53], pp. 3–12 (2022)
Wirsing, M., Hölzl, M. (eds.): Rigorous Software Engineering for Service-Oriented Systems. LNCS, vol. 6582. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20401-2
Wirsing, M., Hölzl, M., Koch, N., Mayer, P. (eds.): Software Engineering for Collective Autonomic Systems. LNCS, vol. 8998. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-16310-9
Acknowledgements
We would like to extend our gratitude to the authors for their valuable contributions, to the reviewers for their expertise and constructive feedback, to the ISOLA chairs, Tiziana Margaria and Bernhard Steffen, for providing us the opportunity to organize this track, and to Springer-Verlag for their invaluable support.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Tribastone, M., Jähnichen, S., Wirsing, M. (2025). Introduction to the REoCAS Colloquium in Honor of Rocco De Nicola’s 70th Birthday. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola. ISoLA 2024. Lecture Notes in Computer Science, vol 15219. Springer, Cham. https://doi.org/10.1007/978-3-031-73709-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-031-73709-1_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-73708-4
Online ISBN: 978-3-031-73709-1
eBook Packages: Computer ScienceComputer Science (R0)