×

Basic observables for a calculus for global computing. (English) Zbl 1119.68124

Summary: We develop the semantic theory of a foundational language for modelling applications over global computers whose interconnection structure can be explicitly manipulated. Together with process distribution, process mobility and remote asynchronous communication through distributed data repositories, the language has primitives for explicitly modelling inter-node connections and for dynamically activating and deactivating them. For the proposed language, we define natural notions of extensional observations and study their closure under operational reductions and/or language contexts to obtain barbed congruence and may testing equivalence. We then focus on barbed congruence and provide an alternative characterisation in terms of a labelled bisimulation. To test practical usability of the semantic theory, we model a system of communicating mobile devices and use the introduced proof techniques to verify one of its key properties.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

KLAIM; Klava; tKlaim; Linda
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amadio, R., On modelling mobility, Theor. Comput. Sci., 240, 1, 147-176 (2000) · Zbl 0954.68072
[2] Amadio, R. M.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous π-calculus, Theor. Comput. Sci., 195, 2, 291-324 (1998) · Zbl 0915.68009
[3] Bettini, L.; De Nicola, R., Mobile distributed programming in X-Klaim, (Formal Methods for Mobile Computing. Formal Methods for Mobile Computing, Lecture Notes in Computer Science, vol. 3465 (2005), Springer), 29-68
[4] Bettini, L.; De Nicola, R.; Ferrari, G.; Pugliese, R., Interactive mobile agents in X-Klaim, (Proc. of the 7th WETICE (1998), IEEE), 110-115
[5] Boreale, M.; De Nicola, R., Testing equivalences for mobile processes, Inform. Comput., 120, 279-303 (1995) · Zbl 0835.68073
[6] Boreale, M.; De Nicola, R.; Pugliese, R., Trace and testing equivalence on asynchronous processes, Inform. Comput., 172, 139-164 (2002) · Zbl 1009.68079
[7] Boreale, M.; De Nicola, R.; Pugliese, R., Basic observables for processes, Inform. Comput., 149, 1, 77-98 (1999) · Zbl 0928.68013
[8] Bugliesi, M.; Crafa, S.; Merro, M.; Sassone, V., Communication and mobility control in boxed ambients, Inform. Comput., 202, 1, 39-86 (2005) · Zbl 1101.68943
[9] Cardelli, L.; Gordon, A. D., Mobile ambients, Theor. Comput. Sci., 240, 1, 177-213 (2000) · Zbl 0954.68108
[10] Castagna, G.; Vitek, J.; Zappa Nardelli, F., The seal calculus, Inform. Comput., 201, 1, 1-54 (2005) · Zbl 1101.68060
[11] Castellani, I.; Hennessy, M., Testing theories for asynchronous languages, (Proc. of FSTTCS’98. Proc. of FSTTCS’98, Lecture Notes in Computer Science, vol. 1530 (1998), Springer), 90-101
[12] De Nicola, R.; Ferrari, G.; Montanari, U.; Pugliese, R.; Tuosto, E., A process calculus for QoS-Aware applications, (Proc. of COORDINATION’05. Proc. of COORDINATION’05, Lecture Notes in Computer Science, vol. 3454 (2005), Springer), 33-48
[13] De Nicola, R.; Ferrari, G.; Pugliese, R., Klaim: a kernel language for agents interaction and mobility, IEEE Trans. Softw. Eng., 24, 5, 315-330 (1998)
[14] De Nicola, R.; Gorla, D.; Pugliese, R., On the expressive power of KLAIM-based calculi, Theor. Comput. Sci., 356, 3, 387-421 (2006) · Zbl 1092.68070
[15] De Nicola, R.; Gorla, D.; Pugliese, R., Basic observables for a calculus for global computing, (Proc. of ICALP’05. Proc. of ICALP’05, Lecture Notes in Computer Science, vol. 3580 (2005), Springer), 1226-1238 · Zbl 1085.68098
[16] De Nicola, R.; Gorla, D.; Pugliese, R., Global computing in a dynamic network of tuple spaces, (Proc. of COORDINATION’05. Proc. of COORDINATION’05, Lecture Notes in Computer Science, vol. 3454 (2005), Springer), 157-172
[17] De Nicola, R.; Hennessy, M., Testing equivalence for processes, Theor. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518
[18] C. Fournet, G. Gonthier, J.-J. Lévy, L. Maranget, D. Rémy, A calculus of mobile agents, in: Proc. of CONCUR’96, Lecture Notes in Computer Science, vol. 1119, 1996, pages 406-421.; C. Fournet, G. Gonthier, J.-J. Lévy, L. Maranget, D. Rémy, A calculus of mobile agents, in: Proc. of CONCUR’96, Lecture Notes in Computer Science, vol. 1119, 1996, pages 406-421.
[19] A. Francalanza, A study of failure in a distributed Π;; A. Francalanza, A study of failure in a distributed Π;
[20] Francalanza, A.; Hennessy, M., A theory of system behaviour in the presence of node and link failures, Lect. Notes Comput. Sci, 3653, 368-382 (2005) · Zbl 1134.68340
[21] Gelernter, D., Generative communication in Linda, ACM Trans. Progr. Lang. Syst., 7, 1, 80-112 (1985) · Zbl 0559.68030
[22] D. Gorla, Semantic Approaches to Global Computing Systems. PhD thesis, Dip. Sistemi ed Informatica, Univ. di Firenze, 2004.; D. Gorla, Semantic Approaches to Global Computing Systems. PhD thesis, Dip. Sistemi ed Informatica, Univ. di Firenze, 2004.
[23] Hennessy, M.; Merro, M.; Rathke, J., Towards a behavioural theory of access and mobility control in distributed systems, Theor. Comput. Sci., 322, 3, 615-669 (2004) · Zbl 1071.68009
[24] Godskesen, J. C.; Hildebrandt, T., Extending howe’s method to early bisimulations for typed mobile embedded resources with local names, (Proc. of FSTTCS’05. Proc. of FSTTCS’05, Lecture Notes in Computer Science, vol. 3821 (2005), Springer), 140-151 · Zbl 1172.68553
[25] Honda, K.; Yoshida, N., On reduction-based process semantics, Theor. Comput. Sci., 152, 2, 437-486 (1995) · Zbl 0871.68122
[26] Merro, M.; Zappa Nardelli, F., Bisimulation proof methods for mobile ambients, J. ACM, 52, 6, 961-1023 (2005) · Zbl 1326.68201
[27] Milner, R., Pure bigraphs: structure and dynamics, Inform. Comput., 204, 1, 60-122 (2006) · Zbl 1093.68067
[28] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, part I/II, Inform. Comput., 100, 1-77 (1992)
[29] Milner, R.; Sangiorgi, D., Barbed bisimulation, (Proc. of ICALP’92. Proc. of ICALP’92, Lecture Notes in Computer Science, vol. 623 (1992), Springer), 685-695 · Zbl 1425.68298
[30] Montanari, U.; Pistore, M., Finite state verification for the asynchronous pi-calculus, (Proc. of TACAS’99. Proc. of TACAS’99, Lecture Notes in Computer Science, vol. 1579 (1999), Springer), 255-269
[31] Orava, F.; Parrow, J., An algebraic verification of a mobile network, Formal Aspects Comput., 4, 497-543 (1992) · Zbl 0782.68081
[32] Parrow, J., An introduction to the pi-calculus, (Handbook of Process Algebra (2001), Elsevier Science), 479-543 · Zbl 1035.68071
[33] D. Sangiorgi, Expressing Mobility in Process Algebras: First-Order and Higher-Order Para-digms. PhD thesis ECS-LFCS-93-266, University of Edinburgh, 1993.; D. Sangiorgi, Expressing Mobility in Process Algebras: First-Order and Higher-Order Para-digms. PhD thesis ECS-LFCS-93-266, University of Edinburgh, 1993.
[34] Sangiorgi, D., Bisimulation in higher-order process calculi, Inform. Comput., 131, 141-178 (1996) · Zbl 0876.68042
[35] Schmitt, A.; Stefani, J.-B., The m-calculus: a higher-order distributed process calculus, (Proc. of POPL’03 (2003), ACM Press), 50-61 · Zbl 1321.68365
[36] Sewell, P., From rewrite rules to bisimulation congruences, Theor. Comput. Sci., 274, 1-2, 183-230 (2002) · Zbl 0992.68122
[37] Unyapoth, A.; Sewell, P., Nomadic Pict: Correct communication infrastructures for mobile computation, (Proc. of POPL’01 (2001), ACM), 116-127 · Zbl 1323.68416
[38] Wischik, L.; Gardner, P., Strong bisimulation for the explicit fusion calculus, (Proc. of FoSSaCS’04. Proc. of FoSSaCS’04, Lecture Notes in Computer Science, vol. 2987 (2004), Springer), 484-498 · Zbl 1126.68512
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.