A principled exploration of coordination models. (English) Zbl 1080.68066
Summary: Coordination is a style of interaction in which information exchange among independent system components is accomplished by means of high-level constructs designed to enhance the degree of decoupling among participants. A decoupled mode of computation is particularly important in the design of mobile systems which emerge dynamically through the composition of independently developed components meeting under unpredictable circumstances and thrust into achieving purposeful cooperative behaviors. This paper examines a range of coordination models tailored for use in mobile computing and shows that the constructs they provide are reducible to simple schema definitions in Mobile UNITY. Intellectually, this exercise contributes to achieving a better operational-level understanding of the relation among several important classes of models of mobility. Pragmatically, this work demonstrates the immediate applicability of Mobile UNITY to the formal specification of coordination constructs supporting mobile computing. Moreover, the resulting schemas are shown to be helpful in reducing the complexity of the formal verification effort.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68M14 | Distributed systems |
References:
| [1] | F. Achermann, M. Lumpe, J.-G. Schneider, O. Nierstrasz, PICCOLA: a small composition language, Formal Methods for Distributed Processing—A Survey of Object-Oriented Approaches, Cambridge University Press, Cambridge, 2001, pp. 403-426.; F. Achermann, M. Lumpe, J.-G. Schneider, O. Nierstrasz, PICCOLA: a small composition language, Formal Methods for Distributed Processing—A Survey of Object-Oriented Approaches, Cambridge University Press, Cambridge, 2001, pp. 403-426. · Zbl 1255.68053 |
| [2] | L. Andrade, J.L. Fiadeiro, J. Gouveia, G. Koutsoukos, Separating computation, coordination, and configuration, J. Software Maintenance and Evolution: Research and Practice (14)(2002) 353-369.; L. Andrade, J.L. Fiadeiro, J. Gouveia, G. Koutsoukos, Separating computation, coordination, and configuration, J. Software Maintenance and Evolution: Research and Practice (14)(2002) 353-369. · Zbl 1017.68026 |
| [3] | Back, R. J.R.; Sere, K., Stepwise refinement of parallel algorithms, Sci. Comput. Programming, 13, 2-3, 133-180 (1990) · Zbl 0705.68057 |
| [4] | Cabri, G.; Leonardi, L.; Zambonelli, F., MARSa programmable coordination architecture for mobile agents, IEEE Internet Comput., 4, 4, 26-35 (2000) |
| [5] | Cardelli, L.; Gordon, A., Mobile ambients, Theoret. Comput. Sci. (Special Issue on Coordination), 240, 1, 177-213 (2000) · Zbl 0954.68108 |
| [6] | N. Davies, S. Wade, A. Friday, G. Blair, Limbo: a tuple space based platform for adaptive mobile applications, in: Proc. Internat. Conf. on Open Distributed Processing/Distributed Platforms (ICODP/ICDP ’97), May 1997, pp. 291-302.; N. Davies, S. Wade, A. Friday, G. Blair, Limbo: a tuple space based platform for adaptive mobile applications, in: Proc. Internat. Conf. on Open Distributed Processing/Distributed Platforms (ICODP/ICDP ’97), May 1997, pp. 291-302. |
| [7] | C. Fournet, G. Gonthier, The reflexive CHAM and the join-calculus, in: Proc. 23rd ACM Symp. on Principles of Programming Languages, 1996, pp. 372-385.; C. Fournet, G. Gonthier, The reflexive CHAM and the join-calculus, in: Proc. 23rd ACM Symp. on Principles of Programming Languages, 1996, pp. 372-385. |
| [8] | Gelernter, D., Generative communication in Linda, ACM Comput. Surv., 7, 1, 80-112 (1985) · Zbl 0559.68030 |
| [9] | Gray, R.; Kotz, D.; Cybenko, G.; Rus, D., D’Agentssecurity in a multiple-language, (Vigna, G., Mobile Agents and Security, Lecture Notes in Computer Science, Vol. 1419 (1998), Springer: Springer Berlin), 154-187 |
| [10] | Hoare, C. A.R., An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-580, 583 (1969) · Zbl 0179.23105 |
| [11] | Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007 |
| [12] | Mascolo, C., MobiSa specification language for mobile systems, (in: Proc. Third Internat. Conf. on Coordination Models and Languages, Vol. 1594 (1999), Springer, Verlag), 37-52 |
| [13] | Mascolo, C.; Picco, G. P.; Roman, G.-C., A fine-grained model for code mobility, (in: Proc. Seventh European Software Engineering Conf. (ESEC), Lecture Notes in Computer Science, Vol. 1687 (September 1999), Springer, Verlag), 39-56 |
| [14] | C. Mascolo, G.P. Picco, G.-C. Roman, CODEWEAVE: Exploring fine-grained mobility of code, Automat. Software Engg. J. 11 (2004) 207-243.; C. Mascolo, G.P. Picco, G.-C. Roman, CODEWEAVE: Exploring fine-grained mobility of code, Automat. Software Engg. J. 11 (2004) 207-243. |
| [15] | McCann, P. J.; Roman, G.-C., Compositional programming abstractions for mobile computing, IEEE Trans. Software Engg., 24, 2, 97-110 (1998) |
| [16] | Milner, R., Communication and Concurrency (1980), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ |
| [17] | Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, parts I and II, Inform. and Comput., 100, 1, 1-77 (1992) · Zbl 0752.68037 |
| [18] | Murphy, A. L.; Picco, G. P.; Roman, G.-C., LIMEa middleware for physical and logical mobility, (Proc. 21st Internat. Conf. on Distributed Systems (April 2001), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 524-533 |
| [19] | A.L. Murphy, G.P. Picco, G.-C. Roman, LIME: a coordination middleware supporting mobility of hosts and agents, Technical Report WUCSE-03-21, Washington University, Department of Computer Science and Engineering, St. Louis, Missouri, 2003.; A.L. Murphy, G.P. Picco, G.-C. Roman, LIME: a coordination middleware supporting mobility of hosts and agents, Technical Report WUCSE-03-21, Washington University, Department of Computer Science and Engineering, St. Louis, Missouri, 2003. |
| [20] | A. Omicini, F. Zambonelli, The TuCSoN coordination model for mobile information agents, in: Proc. First Workshop on Innovative Internet Information Systems, June 1998.; A. Omicini, F. Zambonelli, The TuCSoN coordination model for mobile information agents, in: Proc. First Workshop on Innovative Internet Information Systems, June 1998. |
| [21] | G.P. Picco, A.L. Murphy, G.-C. Roman, Global virtual data structures, Process Coordination and Ubiquitous Computing, CRC Press, Boca Raton, 2002, pp. 11-29.; G.P. Picco, A.L. Murphy, G.-C. Roman, Global virtual data structures, Process Coordination and Ubiquitous Computing, CRC Press, Boca Raton, 2002, pp. 11-29. |
| [22] | Roman, G.-C.; McCann, P. J., A notation and logic for mobile computing, Formal Methods in System Design, 20, 47-68 (2002) · Zbl 0989.68057 |
| [23] | Sewell, P.; Wojciechowski, P.; Pierce, B., Location-independent communication for mobile agentsa two-level architecture, (Bal, H.; Belkhouche, B.; Cardelli, L., Internet Programming Languages, Lecture Notes in Computer Science, Vol. 1686 (1999), Springer: Springer Berlin) |
| [24] | A. Unypoth, P. Sewell, Nomadic pict: correct communication infrastructure for mobile computation, in: Proc. 28th Ann. Symp. on Principles of Programming Languages (POPL’01), 2001.; A. Unypoth, P. Sewell, Nomadic pict: correct communication infrastructure for mobile computation, in: Proc. 28th Ann. Symp. on Principles of Programming Languages (POPL’01), 2001. · Zbl 1323.68416 |
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.
