Skip to main content

Process Calculi for Modelling Mobile, Service-Oriented, and Collective Autonomic Systems

  • Chapter
  • First Online:
Models, Languages, and Tools for Concurrent and Distributed Programming

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11665))

  • 641 Accesses

Abstract

Process-algebraic methods have proven to be excellent tools for designing and analysing concurrent systems. In this paper we review several process calculi and languages developed and studied by Rocco De Nicola and his students and colleagues in the three EU projects AGILE, SENSORIA, and ASCENS. These calculi provide a theoretical basis for engineering mobile, service-oriented, and collective autonomic systems. KLAIM is a framework for distributed mobile agents consisting of a kernel language, a stochastic extension, a logic for specifying properties of mobile applications, and an automatic tool for verifying such properties. In the AGILE project of the EU Global Computing Initiative I, KLAIM served as a the process-algebraic basis for an architectural approach to mobile systems development. For modelling and analysing service-oriented systems, a family of process-algebraic core calculi was developed in the SENSORIA project of the EU Global Computing Initiative II. These calculi address complementary aspects of service-oriented programming such as sessions and correlations. They come with reasoning and analysis techniques, specification and verification tools as well as prototypical analyses of case studies. In the ASCENS project, the language SCEL was developed for modelling and programming systems consisting of interactive autonomic components. SCEL is based on process-algebraic principles and supports formal description and analysis of the behaviours of ensembles of autonomic components.

- Dedicated to Rocco De Nicola -

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Notes

  1. 1.

    AGILE, CRESCCO, DART, DBGLOBE, DEGAS, FLAGS, MIKADO, MRG, MYTHS, PEPITO, PROFUNDIS, SECURE, SOCS (see [4]).

  2. 2.

    The AGILE partners were LMU München (coordinator), Università di Pisa, Università di Firenze, ISTI Pisa, ATX Software SA, Universidade de Lisboa, University of Warsaw (from August 2002), and University of Leicester (from January 2003).

  3. 3.

    AGILE, DEGAS, MIKADO, PROFUNDIS.

  4. 4.

    The SENSORIA partners were LMU München (coordinator), Università di Trento, University of Leicester, University of Warsaw, TU Demark at Lyngby, Università di Pisa, Università di Firenze, Università di Bologna, ISTI Pisa, Universidade de Lisboa, ATX Software SA (ATX II Technologies SA, from October 2006), Telecom Italia S.p.A., Imperial College London, University College London, FAST GmbH (Cirquent GmbH, from 2008), S & N AG Paderborn, Budapest University of Technology and Economics, and MIP Business School of Politecnico di Milano (from March 2007).

  5. 5.

    The ASCENS partners were LMU München (coordinator), Università di Pisa, Università di Firenze, Fraunhofer FIRST (now Fraunhofer FOKUS), VERIMAG Laboratory, Università di Modena e Reggio Emilia, Université Libre de Bruxelles, Ecole Polytechnique Fédérale de Lausanne, Volkswagen AG, Lero - University of Limerick, Zimory GmbH, and ISTI Pisa, and from July 2011 IMT Lucca, Mobsya, and Charles University Prague.

References

  1. AEOLUS: Algorithmic principles for building efficient overlay computers. EU 6th Framework Programme, Integrated Project, 2005-09-01–2009-08-31, Grant 15964. https://cordis.europa.eu/project/rcn/80615/. Accessed 06 January 2019

  2. AGILE: architectures for mobility. EU 5th Framework Programme, Global Computing Initiative, 2002-01-01–2005-04-30, Contract IST-2001-32747. https://cordis.europa.eu/project/rcn/60315/factsheet/en. http://www.pst.ifi.lmu.de/Forschung/projekte/agile/. Accessed 06 Jan 2019

  3. ASCENS: Autonomic component ensembles. EU 7th Framework Programme, Integrated Project, 2010-10-01–2015-03-31, Grant 257414. http://www.ascens-ist.eu/. https://cordis.europa.eu/project/rcn/95141/. Accessed 06 Jan 2019

  4. Global computing: co-operation of autonomous and mobile entities in dynamic environments - IST-2001-6.2.2, Cordis Database, European Commission. https://cordis.europa.eu/programme/rcn/7974/en. Accessed 13 Jan 2019

  5. MOBIUS: Mobility, ubiquity and security for small devices. EU 6th Framework Programme, Integrated Project, 2010-10-01–2009-08-31, Grant 015905. http://software.imdea.org/gbarthe/mobius/. https://cordis.europa.eu/project/rcn/80614/. Accessed 06 Jan 2019

  6. QUANTICOL: A quantitative approach to management and design of collective and adaptive behaviours. EU 7th Framework Programme, Fundamentals of Collective Adaptive Systems, 2013-04-01–2017-03-31, Contract 600708. http://blog.inf.ed.ac.uk/quanticol/. https://cordis.europa.eu/project/rcn/106237/. Accessed 17 Jan 2019

  7. SENSORIA: Software engineering for service-oriented overlay computers. EU 6th Framework Programme, Integrated Project, 2005-09-01–2010-02-28, Grant Id: 16004. http://www.sensoria-ist.eu/. https://cordis.europa.eu/project/rcn/80616/. Accessed 06 Jan 2019

  8. Acciai, L., Bodei, C., Boreale, M., Bruni, R., Vieira, H.T.: Static analysis techniques for session-oriented calculi. In: Wirsing and Hölzl [73], pp. 214–231 (2011)

    Google Scholar 

  9. Alrahman, Y.A., De Nicola, R., Loreti, M., Tiezzi, F., Vigo, R.: A calculus for attribute-based communication. In: Wainwright, R.L., Corchado, J.M., Bechini, A., Hong, J. (eds.) SAC 2015, pp. 1840–1845. ACM (2015)

    Google Scholar 

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

  11. Baier, C., Katoen, J.-P., Hermanns, H.: Approximative symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146–161. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48320-9_12

    Chapter  Google Scholar 

  12. Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Call-by-contract for service discovery, orchestration and recovery. In: Wirsing and Hölzl [73], pp. 232–261 (2011)

    Google Scholar 

  13. Baumeister, H., Knapp, A., Wirsing, M.: Property-driven development. In: SEFM 2004, pp. 96–102. IEEE Computer Society (2004)

    Google Scholar 

  14. Baumeister, H., Koch, N., Kosiuczenko, P., Stevens, P., Wirsing, M.: UML for global computing. In: Priami [64], pp. 1–24 (2003)

    Google Scholar 

  15. Bettini, L., et al.: The Klaim project: theory and practice. In: Priami [64], pp. 88–150 (2003)

    Chapter  Google Scholar 

  16. Bettini, L., De Nicola, R.: Mobile distributed programming in X-Klaim. In: Bernardo, M., Bogliolo, A. (eds.) SFM-Moby 2005. LNCS, vol. 3465, pp. 29–68. Springer, Heidelberg (2005). https://doi.org/10.1007/11419822_2

    Chapter  Google Scholar 

  17. Bettini, L., De Nicola, R., Pugliese, R.: Klava: a Java package for distributed and mobile applications. Softw. Pract. Exper. 32(14), 1365–1394 (2002)

    Article  Google Scholar 

  18. Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. J. ACM 44(2), 201–236 (1997)

    Article  MathSciNet  Google Scholar 

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

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

  21. Bruni, R., Montanari, U., Sassone, V.: Observational congruences for dynamically reconfigurable tile systems. Theor. Comput. Sci. 335(2–3), 331–372 (2005)

    Article  MathSciNet  Google Scholar 

  22. Buscemi, M.G., Montanari, U.: CC-PI: a constraint language for service negotiation and composition. In: Wirsing and Hölzl [73], pp. 262–281 (2011)

    Google Scholar 

  23. Cabri, G., et al.: Self-expression and dynamic attribute-based ensembles in SCEL. In: Margaria and Steffen [59], pp. 147–163 (2014)

    Chapter  Google Scholar 

  24. Caires, L., De Nicola, R., Pugliese, R., Vasconcelos, V.T., Zavattaro, G.: Core calculi for service-oriented computing. In: Wirsing and Hölzl [73], pp. 153–188 (2011)

    Google Scholar 

  25. Cappello, I., et al.: Quantitative analysis of services. In: Wirsing and Hölzl [73], pp. 522–540 (2011)

    Google Scholar 

  26. Carriero, N., Gelernter, D.: Linda in context. Commun. ACM 32, 444–458 (1989)

    Article  Google Scholar 

  27. Cenciarelli, P., Knapp, A., Reus, B., Wirsing, M.: From sequential to multi-threaded Java: an event-based operational semantics. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 75–90. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0000464

    Chapter  Google Scholar 

  28. Cesari, L., De Nicola, R., Pugliese, R., Puviani, M., Tiezzi, F., Zambonelli, F.: Formalising adaptation patterns for autonomic ensembles. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 100–118. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07602-7_8

    Chapter  Google Scholar 

  29. De Nicola, R., Ferrari, G.L., Pugliese, R.: KLAIM: a kernel language for agents interaction and mobility. IEEE TSE 24, 315–330 (1998)

    Google Scholar 

  30. De Nicola, R.: Testing equivalences and fully abstract models for communicating systems. Ph.D. thesis, University of Edinburgh, UK (1986)

    Google Scholar 

  31. De Nicola, R., Ferrari, G., Montanari, U., Pugliese, R., Tuosto, E.: A formal basis for reasoning on programmable QoS. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 436–479. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39910-0_21

    Chapter  Google Scholar 

  32. de Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 548–560. Springer, Heidelberg (1983). https://doi.org/10.1007/BFb0036936

    Chapter  Google Scholar 

  33. De Nicola, R., Hennicker, R.: A homage to Martin Wirsing. In: Software, Services, and Systems [34], pp. 1–12 (2015)

    Google Scholar 

  34. De Nicola, R., Hennicker, R. (eds.): Software, Services, and Systems. LNCS, vol. 8950. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-319-15545-6

    Book  Google Scholar 

  35. De Nicola, R., Jähnichen, S., Wirsing, M.: Rigorous engineering of collective adaptive systems - introduction to the 2nd track edition. In: Margaria and Steffen [60], pp. 3–12 (2018)

    Google Scholar 

  36. De Nicola, R., Katoen, J., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theor. Comput. Sci. 382(1), 42–70 (2007)

    Article  MathSciNet  Google Scholar 

  37. De Nicola, R., et al.: The SCEL language: design, implementation, verification. In: Wirsing et al. [74], pp. 3–71 (2011)

    Google Scholar 

  38. De Nicola, R., Latella, D., Loreti, M., Massink, M.: MarCaSPiS: a Markovian extension of a calculus for services. Electr. Notes Theor. Comput. Sci. 229(4), 11–26 (2009)

    Article  Google Scholar 

  39. De Nicola, R., Latella, D., Loreti, M., Massink, M.: Sosl: a service-oriented stochastic logic. In: Wirsing and Hölzl [73], pp. 447–466 (2011)

    Google Scholar 

  40. De Nicola, R., Latella, D., Massink, M.: Formal modeling and quantitative analysis of KLAIM-based mobile systems. In: Haddad, H., Liebrock, L.M., Omicini, A., Wainwright, R.L. (eds.) ACM Symposium on Applied Computing (SAC), pp. 428–435. ACM (2005)

    Google Scholar 

  41. De Nicola, R., Loreti, M.: MoMo: a modal logic for reasoning about mobility. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 95–119. Springer, Heidelberg (2005). https://doi.org/10.1007/11561163_5

    Chapter  MATH  Google Scholar 

  42. De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A formal approach to autonomic systems programming: the SCEL language. TAAS 9(2), 7:1–7:29 (2014)

    Article  Google Scholar 

  43. De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation (extended abstract). In: LICS, pp. 118–129 (1990)

    Google Scholar 

  44. Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A model checking approach for verifying COWS specifications. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 230–245. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78743-3_17

    Chapter  Google Scholar 

  45. Ferrari, G.L., Gnesi, S., Montanari, U., Pistore, M.: A model-checking verification environment for mobile processes. ACM Trans. Softw. Eng. Methodol. 12(4), 440–473 (2003)

    Article  Google Scholar 

  46. Ferrari, G.L., Gnesi, S., Montanari, U., Raggi, R., Trentanni, G., Tuosto, E.: Verification on the web of mobile systems. In: Augusto, J.C., Ultes-Nitsche, U. (eds.) VVEIS 2004, pp. 72–74. INSTICC Press (2004)

    Google Scholar 

  47. Ferrari, G.L., Moggi, E., Pugliese, R.: MetaKlaim: a type safe multi-stage language for global computing. Math. Struct. Comput. Sci. 14(3), 367–395 (2004)

    Article  MathSciNet  Google Scholar 

  48. Fiadeiro, J.L., Lopes, A.: CommUnity on the move: architectures for distribution and mobility. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 177–196. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30101-1_8

    Chapter  MATH  Google Scholar 

  49. Gelernter, D.: Generative communication in Linda. TOPLAS 7, 80–112 (1985)

    Article  Google Scholar 

  50. Guidi, C.: Formalizing languages for service-oriented computing. Ph.D. thesis, Universita di Bologna (2007)

    Google Scholar 

  51. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)

    Article  MathSciNet  Google Scholar 

  52. Hölzl, M.M., Rauschmayer, A., Wirsing, M.: Engineering of software-intensive systems: state of the art and research challenges. In: Wirsing et al. [69], pp. 1–44 (2008)

    MATH  Google Scholar 

  53. Knapp, A., Merz, S., Wirsing, M., Zappe, J.: Specification and refinement of mobile systems in MTLA and mobile UML. Theor. Comput. Sci. 351(2), 184–202 (2006)

    Article  MathSciNet  Google Scholar 

  54. Kozen, D.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27, 333–354 (1983)

    Article  MathSciNet  Google Scholar 

  55. Krutisch, R., Meier, P., Wirsing, M.: The AgentComponent approach, combining agents, and components. In: Schillo, M., Klusch, M., Müller, J., Tianfield, H. (eds.) MATES 2003. LNCS (LNAI), vol. 2831, pp. 1–12. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39869-1_1

    Chapter  Google Scholar 

  56. Lanese, I., Martins, F., Vasconcelos, V.T., Ravara, A.: Disciplining orchestration and conversation in service-oriented computing. In: SEFM 2007, pp. 305–314. IEEE Computer Society (2007)

    Google Scholar 

  57. Latella, D., Massink, M., Baumeister, H., Wirsing, M.: Mobile UML statecharts with localities. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 34–58. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31794-4_3

    Chapter  Google Scholar 

  58. Loreti, M., Hillston, J.: Modelling and analysis of collective adaptive systems with CARMA and its tools. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 83–119. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-34096-8_4

    Chapter  Google Scholar 

  59. Margaria, T., Steffen, B. (eds.): ISoLA 2014. LNCS, vol. 8802. Springer, Heidelberg (2014)

    Google Scholar 

  60. Margaria, T., Steffen, B. (eds.): ISoLA 2018, Proceedings, Part III. LNCS, vol. 11246. Springer, Heidelberg (2018). https://doi.org/10.1007/978-3-030-03424-5

    Book  Google Scholar 

  61. Milner, R.: Communicating and Mobile Systems: the \(\pi \)-Calculus. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  62. Misra, J., Cook, W.R.: Computation orchestration. Softw. Syst. Model. 6(1), 83–110 (2007)

    Article  Google Scholar 

  63. OASIS: eXtensible Access Control Markup Language (XACML) version 3.0, January 2013. http://docs.oasis-open.org/xacml/3.0/xacml-3.0-core-spec-os-en.pdf. Accessed 22 Jan 2019

  64. Priami, C. (ed.): GC 2003. Lecture Notes in Computer Science, vol. 2874. Springer, Heidelberg (2003). https://doi.org/10.1007/b94264

    Book  MATH  Google Scholar 

  65. Pugliese, R., Tiezzi, F.: A calculus for orchestration of web services. J. Appl. Log. 10(1), 2–31 (2007)

    Article  MathSciNet  Google Scholar 

  66. Sestini, F., Hogenhout, W.: A report on the FET global computing initiative. European Commission, DG Information Society, Future and Emerging Technologies (2005)

    Google Scholar 

  67. ter Beek, M.H.: SENSORIA results applied to the case studies. In: Wirsing and Hölzl [73], pp. 655–677 (2011)

    Google Scholar 

  68. Vieira, H.T., Caires, L., Seco, J.C.: The conversation calculus: a model of service-oriented computation. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 269–283. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78739-6_21

    Chapter  Google Scholar 

  69. Wirsing, M., Banâtre, J., Hölzl, M.M., Rauschmayer, A. (eds.): Software-Intensive Systems and New Computing Paradigms - Challenges and Visions. LNCS, vol. 5380. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89437-7

    Book  MATH  Google Scholar 

  70. Wirsing, M., et al.: Semantic-based development of service-oriented systems. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 24–45. Springer, Heidelberg (2006). https://doi.org/10.1007/11888116_3

    Chapter  Google Scholar 

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

  72. Wirsing, M., De Nicola, R., Hölzl, M.M.: Introduction to ‘rigorous engineering of autonomic ensembles’- track introduction. In: Margaria and Steffen [59], pp. 96–98 (2014)

    Chapter  Google Scholar 

  73. Wirsing, M., Hölzl, M.M. (eds.): Rigorous Software Engineering for Service-Oriented Systems - Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing. LNCS, vol. 6582. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20401-2

    Book  Google Scholar 

  74. Wirsing, M., Hölzl, M.M., Koch, N., Mayer, P. (eds.): Software Engineering for Collective Autonomic Systems - The ASCENS Approach. LNCS, vol. 8998. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-319-16310-9

    Book  Google Scholar 

  75. Wirsing, M., Hölzl, M., Tribastone, M., Zambonelli, F.: ASCENS: engineering autonomic service-component ensembles. In: Beckert, B., Damiani, F., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2011. LNCS, vol. 7542, pp. 1–24. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35887-6_1

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding authors

Correspondence to Martin Wirsing or Rolf Hennicker .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Wirsing, M., Hennicker, R. (2019). Process Calculi for Modelling Mobile, Service-Oriented, and Collective Autonomic Systems. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds) Models, Languages, and Tools for Concurrent and Distributed Programming. Lecture Notes in Computer Science(), vol 11665. Springer, Cham. https://doi.org/10.1007/978-3-030-21485-2_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-21485-2_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-21484-5

  • Online ISBN: 978-3-030-21485-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics