Top

Published in:

2019 | OriginalPaper | Chapter

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

Authors : Martin Wirsing, Rolf Hennicker

Published in: Models, Languages, and Tools for Concurrent and Distributed Programming

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Event Structure Semantics for Multiparty Sessions

next chapter Autonomous Systems – An Architectural Characterization

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

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

AGILE, DEGAS, MIKADO, PROFUNDIS.

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

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.

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)

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_1CrossRef

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_12CrossRef

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)

13.

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

14.

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

15.

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

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_2CrossRef

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)CrossRef

18.

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

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_3CrossRef

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_3CrossRef

21.

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

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)

23.

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

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)

25.

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

26.

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

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/BFb0000464CrossRef

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_8CrossRef

29.

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

30.

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

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_21CrossRef

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/BFb0036936CrossRef

33.

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

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

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)

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)MathSciNetCrossRef

37.

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

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)CrossRef

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)

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)

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_5CrossRefMATH

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)CrossRef

43.

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

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_17CrossRef

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)CrossRef

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)

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)MathSciNetCrossRef

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_8CrossRefMATH

49.

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

50.

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

51.

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

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

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)MathSciNetCrossRef

54.

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

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_1CrossRef

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)

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_3CrossRef

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_4CrossRef

59.

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

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

61.

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

62.

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

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/b94264CrossRefMATH

65.

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

66.

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

67.

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

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_21CrossRef

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

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_3CrossRef

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_3CrossRef

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)CrossRef

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

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

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_1CrossRef

Title: Process Calculi for Modelling Mobile, Service-Oriented, and Collective Autonomic Systems
Authors: Martin Wirsing
Rolf Hennicker
Publisher: Springer International Publishing
Book: Models, Languages, and Tools for Concurrent and Distributed Programming
Print ISBN: 978-3-030-21484-5

Electronic ISBN: 978-3-030-21485-2

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-21485-2_20

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner