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 -
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
AGILE, CRESCCO, DART, DBGLOBE, DEGAS, FLAGS, MIKADO, MRG, MYTHS, PEPITO, PROFUNDIS, SECURE, SOCS (see [4]).
- 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.
AGILE, DEGAS, MIKADO, PROFUNDIS.
- 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.
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
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
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
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
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
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
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
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
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)
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)
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
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
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)
Baumeister, H., Knapp, A., Wirsing, M.: Property-driven development. In: SEFM 2004, pp. 96–102. IEEE Computer Society (2004)
Baumeister, H., Koch, N., Kosiuczenko, P., Stevens, P., Wirsing, M.: UML for global computing. In: Priami [64], pp. 1–24 (2003)
Bettini, L., et al.: The Klaim project: theory and practice. In: Priami [64], pp. 88–150 (2003)
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
Bettini, L., De Nicola, R., Pugliese, R.: Klava: a Java package for distributed and mobile applications. Softw. Pract. Exper. 32(14), 1365–1394 (2002)
Bistarelli, S., Montanari, U., Rossi, F.: Semiring-based constraint satisfaction and optimization. J. ACM 44(2), 201–236 (1997)
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
Bruni, R., Montanari, U., Sassone, V.: Observational congruences for dynamically reconfigurable tile systems. Theor. Comput. Sci. 335(2–3), 331–372 (2005)
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)
Cabri, G., et al.: Self-expression and dynamic attribute-based ensembles in SCEL. In: Margaria and Steffen [59], pp. 147–163 (2014)
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)
Cappello, I., et al.: Quantitative analysis of services. In: Wirsing and Hölzl [73], pp. 522–540 (2011)
Carriero, N., Gelernter, D.: Linda in context. Commun. ACM 32, 444–458 (1989)
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
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
De Nicola, R., Ferrari, G.L., Pugliese, R.: KLAIM: a kernel language for agents interaction and mobility. IEEE TSE 24, 315–330 (1998)
De Nicola, R.: Testing equivalences and fully abstract models for communicating systems. Ph.D. thesis, University of Edinburgh, UK (1986)
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
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
De Nicola, R., Hennicker, R.: A homage to Martin Wirsing. In: Software, Services, and Systems [34], pp. 1–12 (2015)
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
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)
De Nicola, R., Katoen, J., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theor. Comput. Sci. 382(1), 42–70 (2007)
De Nicola, R., et al.: The SCEL language: design, implementation, verification. In: Wirsing et al. [74], pp. 3–71 (2011)
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)
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)
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)
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
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)
De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation (extended abstract). In: LICS, pp. 118–129 (1990)
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
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)
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)
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)
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
Gelernter, D.: Generative communication in Linda. TOPLAS 7, 80–112 (1985)
Guidi, C.: Formalizing languages for service-oriented computing. Ph.D. thesis, Universita di Bologna (2007)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)
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)
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)
Kozen, D.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27, 333–354 (1983)
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
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)
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
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
Margaria, T., Steffen, B. (eds.): ISoLA 2014. LNCS, vol. 8802. Springer, Heidelberg (2014)
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
Milner, R.: Communicating and Mobile Systems: the \(\pi \)-Calculus. Cambridge University Press, Cambridge (1999)
Misra, J., Cook, W.R.: Computation orchestration. Softw. Syst. Model. 6(1), 83–110 (2007)
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
Priami, C. (ed.): GC 2003. Lecture Notes in Computer Science, vol. 2874. Springer, Heidelberg (2003). https://doi.org/10.1007/b94264
Pugliese, R., Tiezzi, F.: A calculus for orchestration of web services. J. Appl. Log. 10(1), 2–31 (2007)
Sestini, F., Hogenhout, W.: A report on the FET global computing initiative. European Commission, DG Information Society, Future and Emerging Technologies (2005)
ter Beek, M.H.: SENSORIA results applied to the case studies. In: Wirsing and Hölzl [73], pp. 655–677 (2011)
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
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
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
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.: Introduction to ‘rigorous engineering of autonomic ensembles’- track introduction. In: Margaria and Steffen [59], pp. 96–98 (2014)
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
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
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
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
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)