Formal Specification and Verification of Mobile Agent Systems

Laid Kahloul, Messaouda Grira


Mobile agent systems offer efficiency and flexibility as a design paradigm. These two characteristics allow to these systems to be an adequate solution for many problems. These systems are used in many critical domains. This expansion, in use, obliges designers to insure the reliability and correctness of such systems. Formal methods can be used to verify the
correctness of these systems. This paper presents a formal specification and verification of mobile agent systems using the High Order π-calculus. The verification exploits the two
tools UPPAAL and SPIN.


Mobile Agent, Formal Verification, pi-calculus, Promela, SPIN, UPPAAL.

Full Text:



Robin Milner., Communication and Concurrency, Prentice Hall, International Series in Computer Science, ISBN 0-13-115007-3. 1989.

Nicholas Rescher, James Garson,Topological Logic, in The Journal of Symbolic Logic, 33(4). pp. 537-548, December, 1968.

Wagner, F., Modeling Software with Finite State Machines: A Practical Approach, Auerbach Publications, 2006, ISBN 0-8493-8086-3.

Tadao Murata., Petri Nets: Properties, Analysis and Applications, in Proceedings of the IEEE, vol. 77, no. 4, April 1989.

Fuggetta, A., Picco, G.P., and Vigna, G., Understanding Code Mobility, IEEE transactions on software engineering, vol. 24, no. 5, may 1998.

Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi, Uppaal - a Tool Suite for Automatic Verification of Real-Time Systems, in Proceedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, New Brunswick, New Jersey, 22-24 October, 1995.

Andreea Barbu., Developing Mobiles Agents Through a Formal Approach, Thesis, Paris XII, 12 September 2005.

A. V. Lamsweerd., Formal Specification: a Roadmap, ICSE '00 Proceedings of the Conference on The Future of Software Engineering. pp. 147-159, 2000.

A. B. Gurdag and M. U. Caglayan, A Formal Security Analysis of SAODV using Model Checking, International Symposium on Computer Networks (ISCN), June 2008.

D. Sangiorgi and D. Walker., The Pi-calculus: A Theory of Mobile Process, Cambridge University Press, 2003.

Faez CHARFI., Une approche dinterfaage de CoD UPPAAL pour la spcification et la vrification des systmes temps rel, Thesis, September 2003.

Theo Ruys., SPIN and Promela, January 18, 2006.

Mihaela Sighireanu., LOTOS NT User Manual, February 21, 2008.

Robert S. Gray,George Cybenko, David Kotz, Ronald A. Peterson, and Daniela Rus., d'agents: Application and performance of a mobile-agent system, 2002.

Akhil Sahai and Christine Morin., Mobile agents for enabling mobile user aware application, Proceedings of the 2nd International Conference on Autonomous agents, pp. 205-211, 1998.

Kharthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter., Formal Verification of Standards for Distance Vector, Journal of the ACM, Vol. 49, pp. 538576, July 4, 2002.

Gian Pietro Picco., Understanding, Evaluating, Formalizing, and Exploiting Code Mobility, Ph.D. Thesis, Politecnico di Torino, Italy, February 1998.

Ichiro Satoh., Physical mobility and Logical mobility in ubiquitous computing environments Proceeding MA '02 Proceedings of the 6th International Conference on Mobile Agents, 2002.

Dag Johansen., Mobile agents: Right concept, wrong approach, Mobile Data Management-MDM, pp. 300-301, 2004.

Sergi Robles., Mobile Agent Systems and Trust, a Combined View Toward Secure Sea-of-Data Applications, Barcelona: s.n., July 2002.

D.Kotz and R. S. Gray., Mobile agents and the Future of internet, Operating Systems Review 1999.

Volker Roth., Obstacles to adoption of mobile agents, IEEE International Conference on Mobile Data Management, 2004.

Dejan Milojicic., Mobile agent applications, Trend Wars: Mobile agent applications. IEEE Concurrency, 1999: 80 90, July 1999.

D. Sangiorgi., From π-calculus to Higher-Order-π-calculus- and back. TAPSOFT '93 Proceedings of the International Joint Conference CAAP/FASE on Theory and Practice of Software Development, 1993.

R.Milner, J.Parrow and D.Walker., A calculus of mobile processes, part I/II. 1992.

C.Perkins E. Guttman., Service Location Protocol (SLP), online:

Prabhu Shankar Kaliappan., Simple Promela Interpretor (SPIN)- Model Checker.

Sadegh Guillaume., A Promela front-end for Spot, May 2008.

Rajeev Alur and David L. Dill., Automata for modeling real-time systems, Colloquium on Algorithms, Languages, and Programming, Vol. 443, pp. 322335, 1990.

John E. Hopcroft and Jeffrey D. Ullman., Introduction of Automata Theory, Languages, s.l. : Addison Wesley, 2001.

Michael Huth and Mark Ryan., Logic in Computer Science, (Second Edition), Cambridge University Press. p. 207. ISBN 0-521-54310-X. 2004.

Kahloul, L. and Chaoui, A., Coloured Reconfigurable Nets for Code Mobility Modeling, In the International Journal of Computers, Communications and Control, ISSN 1841-9836, E-ISSN 1841-9844. Vol. III (2008), Suppl. issue: Proceedings of ICCCC 2008. pp 358- 363.

Kahloul, L, Chaoui, A and Djouani, K., Code Mobility Modelling: A Formal Study, In International Review on Computer and Software, may 2009.

Kahloul Laid, Chaoui Allaoua and Djouani Karim, Modeling Reconfirgurable Systems Using Flexible Petri Nets, In 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, August 24 - 27, 2010, Taipei, Taiwan.


Copyright (c) 2017 Laid Kahloul, Messaouda Grira

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.

CC-BY-NC  License for Website User

Articles published in IJCCC user license are protected by copyright.

Users can access, download, copy, translate the IJCCC articles for non-commercial purposes provided that users, but cannot redistribute, display or adapt:

  • Cite the article using an appropriate bibliographic citation: author(s), article title, journal, volume, issue, page numbers, year of publication, DOI, and the link to the definitive published version on IJCCC website;
  • Maintain the integrity of the IJCCC article;
  • Retain the copyright notices and links to these terms and conditions so it is clear to other users what can and what cannot be done with the  article;
  • Ensure that, for any content in the IJCCC article that is identified as belonging to a third party, any re-use complies with the copyright policies of that third party;
  • Any translations must prominently display the statement: "This is an unofficial translation of an article that appeared in IJCCC. Agora University  has not endorsed this translation."

This is a non commercial license where the use of published articles for commercial purposes is forbiden. 

Commercial purposes include: 

  • Copying or downloading IJCCC articles, or linking to such postings, for further redistribution, sale or licensing, for a fee;
  • Copying, downloading or posting by a site or service that incorporates advertising with such content;
  • The inclusion or incorporation of article content in other works or services (other than normal quotations with an appropriate citation) that is then available for sale or licensing, for a fee;
  • Use of IJCCC articles or article content (other than normal quotations with appropriate citation) by for-profit organizations for promotional purposes, whether for a fee or otherwise;
  • Use for the purposes of monetary reward by means of sale, resale, license, loan, transfer or other form of commercial exploitation;

    The licensor cannot revoke these freedoms as long as you follow the license terms.

[End of CC-BY-NC  License for Website User]

INTERNATIONAL JOURNAL OF COMPUTERS COMMUNICATIONS & CONTROL (IJCCC), With Emphasis on the Integration of Three Technologies (C & C & C),  ISSN 1841-9836.

IJCCC was founded in 2006,  at Agora University, by  Ioan DZITAC (Editor-in-Chief),  Florin Gheorghe FILIP (Editor-in-Chief), and  Misu-Jan MANOLESCU (Managing Editor).

Ethics: This journal is a member of, and subscribes to the principles of, the Committee on Publication Ethics (COPE).

Ioan  DZITAC (Editor-in-Chief) at COPE European Seminar, Bruxelles, 2015:

IJCCC is covered/indexed/abstracted in Science Citation Index Expanded (since vol.1(S),  2006); JCR2018: IF=1.585..

IJCCC is indexed in Scopus from 2008 (CiteScore2018 = 1.56):

Nomination by Elsevier for Journal Excellence Award Romania 2015 (SNIP2014 = 1.029): Elsevier/ Scopus

IJCCC was nominated by Elsevier for Journal Excellence Award - "Scopus Awards Romania 2015" (SNIP2014 = 1.029).

IJCCC is in Top 3 of 157 Romanian journals indexed by Scopus (in all fields) and No.1 in Computer Science field by Elsevier/ Scopus.


 Impact Factor in JCR2018 (Clarivate Analytics/SCI Expanded/ISI Web of Science): IF=1.585 (Q3). Scopus: CiteScore2018=1.56 (Q2);

SCImago Journal & Country Rank

Editors-in-Chief: Ioan DZITAC & Florin Gheorghe FILIP.