A practical approach to specifying and verifying mobile agent algorithms

Xuhui Li, Zhiyong Peng, Jiannong Cao

Research output: Journal article publicationJournal articleAcademic researchpeer-review

2 Citations (Scopus)


Mobile agent, as a new mobile computing technology, has been applied to various parallel and distributed computing problem solutions. Several mobile agent systems have been built to drive the agents following a platform dependant scheme, and some formal approaches have been proposed to describe mobile agents' behaviors or properties for respective purposes. However, there remains a lack of a standard approach to describing a mobile agent algorithm and its semantics from the viewpoint of a practical program, which makes it difficult to specify an algorithm unambiguously and verify its correctness formally. This paper proposes a practical approach to overcome that difficulty by defining a script language and associated mechanisms to specify and verify mobile agent algorithms. The language, called SMAL, can describe mobile agent's behaviors clearly due to its explicitly defined semantics. Based on the semantics, a transformation function for converting the specified algorithm to its equivalent specification in Mobile UNITY, a well-known mobile computation formal approach for correctness verification, is presented. Formal verification of the algorithms can be accomplished based on the UNITY-logic rules.
Original languageEnglish
Pages (from-to)115-122
Number of pages8
JournalInternational Journal of Pervasive Computing and Communications
Issue number2
Publication statusPublished - 1 May 2005


  • Correctness verification
  • Mobile agent

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this