Please use this identifier to cite or link to this item: http://hdl.handle.net/10397/18831
Title: A practical approach to specifying and verifying mobile agent algorithms
Authors: Li, X
Peng, Z
Cao, J 
Keywords: Correctness verification
Mobile agent
Issue Date: 2005
Source: International journal of pervasive computing and communications, 2005, v. 1, no. 2, p. 115-122 How to cite?
Journal: International Journal of Pervasive Computing and Communications 
Abstract: 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.
URI: http://hdl.handle.net/10397/18831
ISSN: 1742-7371
DOI: 10.1108/17427370580000117
Appears in Collections:Journal/Magazine Article

Access
View full-text via PolyU eLinks SFX Query
Show full item record

SCOPUSTM   
Citations

2
Last Week
0
Last month
0
Citations as of Nov 15, 2017

Page view(s)

33
Last Week
1
Last month
Checked on Nov 13, 2017

Google ScholarTM

Check

Altmetric



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.