Formalizing Properties of Mobile Agent Systems
The wide-spreading of Internet has stimulated the introduction of new programming paradigms and languages that model interactions among hosts by means of mobile agents, and that are centered around the notions of location awareness. In this paper we show how to use formal tools, specifically a modal logic, for formalizing properties for mobile agent systems. We concentrate on one of these new languages, Klaim, and we use it to specify a system that permits maintaining the software installed on several heterogeneous computers distributed over a network by taking advantage of the mobile agent paradigm.
KeywordsModal Logic Mobile Agent Private Locality Abstract Action Formal Tool
Unable to display preview. Download preview PDF.
- 1.L. Bettini, R. De Nicola, G. Ferrari, and R. Pugliese. Interactive Mobile Agents in X-Klaim. In P. Ciancarini and R. Tolksdorf, editors, Proc. of the 7th Int. IEEE Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), pages 110–115. IEEE Computer Society Press, 1998.Google Scholar
- 2.L. Bettini, R. De Nicola, and M. Loreti. Software Update via Mobile Agent Based Programming. In Proc. of ACM SAC 2002, Special Track on Agents, Interactions, Mobility, and Systems. ACM Press, 2002. To appear.Google Scholar
- 3.L. Caires and L. Cardelli. A Spatial Logic for Concurrency (Part I). In proceeding of TACS2001, 2001. to appear.Google Scholar
- 5.L. Cardelli and A. D. Gordon. Anytime, Anywhere: Modal Logics for Mobile Ambients. In 27th Annual Symposium on Principles of Programming Languages (POPL) (Boston, MA). ACM, 2000.Google Scholar
- 6.L. Cardelli and A. D. Gordon. Logical Properties of Name Restriction. In proceeding of TLCA’01, volume 2044 of Lecure Note in Computer Science. Springer, 2001.Google Scholar
- 8.A. Carzaniga, G. Picco, and G. Vigna. Designing Distributed Applications with Mobile Code Paradigms. In R. Taylor, editor, Proc. of the 19th Int. Conf. on Software Engineering (ICSE’ 97), pages 22–33. ACM Press, 1997.Google Scholar
- 11.R. De Nicola and M. Loreti. A Modal Logic for Mobile Agents. Technical report, Dipartimento di Sistemi ed Informatica, Universitá degli Studi di Firenze, 2001. available at http://music.dsi.unifi.it/.
- 13.C. Harrison, D. Chess, and A. Kershenbaum. Mobile agents: Are they a good idea? Research Report 19887, IBM Research Division, 1994.Google Scholar
- 15.F. Knabe. An overview of mobile agent programming. In Proceedings of the Fifth LOMAPS workshop on Analysis and Veri.cation of Multiple—Agent Languages, number 1192 in LNCS. Springer-Verlag, 1996.Google Scholar
- 17.X. Leroy, D. Rémy, J. Vouillon, and D. Doligez. The Objective Caml system, documentation and user’s guide. http://caml.inria.fr/ocaml/htmlman/, 1999.
- 18.M. Loreti. Languages and Logics for Network Aware Programming. PhD thesis, Università di Siena, 2002. Available at http://music.dsi.unifi.it.
- 19.R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
- 20.R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Part I. LFCS Report Series ECS-LFCS-89-85, University of Edinburgh, June 1989.Google Scholar
- 21.R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Part II. LFCS Report Series ECS-LFCS-89-86, University of Edinburgh, June 1989.Google Scholar
- 23.A. Park and P. Reichl. Personal Disconnected Operations with Mobile Agents. In Proc. of 3rd Workshop on Personal Wireless Communications, PWC’98, 1998.Google Scholar
- 25.J. E. White. Telescript Technology: The Foundation for the Electronic Marketplace. White paper, General Magic, Inc., Mountain View, CA, 1994.Google Scholar
- 26.J. E. White. Mobile Agents. In J. Bradshaw, editor, Software Agents. AAAI Press and MIT Press, 1996.Google Scholar