A practical approach to specifying and verifying mobile agent algorithms

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.