iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/978-3-031-73709-1_1
Introduction to the REoCAS Colloquium in Honor of Rocco De Nicola’s 70th Birthday | SpringerLink
Skip to main content

Introduction to the REoCAS Colloquium in Honor of Rocco De Nicola’s 70th Birthday

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola (ISoLA 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 15219))

Included in the following conference series:

  • 88 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abd Alrahman, Y., De Nicola, R., Loreti, M.: A calculus for collective-adaptive systems and its behavioural theory. Inf. Comput. 268, 104457 (2019)

    Article  MathSciNet  Google Scholar 

  2. 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

  3. 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

    Chapter  Google Scholar 

  4. 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

  5. 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

  6. 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

    Chapter  Google Scholar 

  7. 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

  8. 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

  9. 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

    Chapter  Google Scholar 

  10. 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

    Chapter  Google Scholar 

  11. 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

  12. 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

    Book  Google Scholar 

  13. 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)

    Google Scholar 

  14. 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)

    Google Scholar 

  15. 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

  16. 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

  17. 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)

    Google Scholar 

  18. 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

  19. 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

    Chapter  Google Scholar 

  20. 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)

    Article  Google Scholar 

  21. 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

    Chapter  Google Scholar 

  22. 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)

    Article  Google Scholar 

  23. 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)

    Article  Google Scholar 

  24. 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

  25. 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

  26. 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)

    Article  Google Scholar 

  27. 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)

    Google Scholar 

  28. 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

    Google Scholar 

  29. 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)

    Article  Google Scholar 

  30. 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

  31. 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)

    Google Scholar 

  32. 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

    Chapter  Google Scholar 

  33. 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

  34. De Nicola, R.: Extensional equivalences for transition systems. Acta Informatica 24(2), 211–237 (1987)

    Article  MathSciNet  Google Scholar 

  35. 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)

    Google Scholar 

  36. 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)

    Article  MathSciNet  Google Scholar 

  37. 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)

    Article  Google Scholar 

  38. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theoret. Comput. Sci. 34(1), 83–133 (1984)

    Article  MathSciNet  Google Scholar 

  39. 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)

    Google Scholar 

  40. De Nicola, R., Loreti, M.: A modal logic for mobile agents. ACM Trans. Comput. Logic (TOCL) 5(1), 79–128 (2004)

    Article  MathSciNet  Google Scholar 

  41. 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)

    Google Scholar 

  42. De Nicola, R., Melgratti, H.: Multiparty testing preorders. Logical Methods Comput. Sci. 19 (2023)

    Google Scholar 

  43. 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)

    Article  Google Scholar 

  44. 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

  45. 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

    Chapter  Google Scholar 

  46. 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

  47. 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

  48. 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

    Chapter  Google Scholar 

  49. 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)

    Article  Google Scholar 

  50. 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

  51. 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

  52. Margaria, T., Steffen, B. (eds.): ISoLA 2014. LNCS, vol. 8802. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45234-9

    Book  Google Scholar 

  53. Margaria, T., Steffen, B. (eds.): ISoLA 2014. LNCS, vol. 13703. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-031-19759-8

  54. 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

    Chapter  Google Scholar 

  55. 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

  56. 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

  57. 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)

    Google Scholar 

  58. 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

  59. 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

  60. 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

  61. 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)

    Google Scholar 

  62. Soderi, S., De Nicola, R.: 6G networks physical layer security using RGB visible light communications. IEEE Access 10, 5482–5496 (2022)

    Article  Google Scholar 

  63. 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

  64. 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)

    Article  Google Scholar 

  65. 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)

    Google Scholar 

  66. 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)

    Article  Google Scholar 

  67. 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

    Chapter  Google Scholar 

  68. Wirsing, M., De Nicola, R., Hölzl, M.M.: Rigorous engineering of autonomic ensembles – track introduction. In: [52], pp. 96–98 (2014)

    Google Scholar 

  69. 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)

    Google Scholar 

  70. 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

    Book  Google Scholar 

  71. 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

    Book  Google Scholar 

Download references

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

Authors

Corresponding author

Correspondence to Martin Wirsing .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics