{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T18:04:54Z","timestamp":1754157894563,"version":"3.41.2"},"reference-count":16,"publisher":"Emerald","issue":"2","license":[{"start":{"date-parts":[[2005,5,1]],"date-time":"2005-05-01T00:00:00Z","timestamp":1114905600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.emerald.com\/insight\/site-policies"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005,5,1]]},"abstract":"<jats:p>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\u2019 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\u2019s 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\u2010known mobile computation formal approach for correctness verification, is presented. Formal verification of the algorithms can be accomplished based on the UNITY\u2010logic rules.<\/jats:p>","DOI":"10.1108\/17427370580000117","type":"journal-article","created":{"date-parts":[[2010,6,5]],"date-time":"2010-06-05T07:20:05Z","timestamp":1275722405000},"page":"115-122","source":"Crossref","is-referenced-by-count":1,"title":["A practical approach to specifying and verifying mobile agent algorithms"],"prefix":"10.1108","volume":"1","author":[{"given":"Xuhui","family":"Li","sequence":"first","affiliation":[]},{"given":"Zhiyong","family":"Peng","sequence":"additional","affiliation":[]},{"given":"Jiannong","family":"Cao","sequence":"additional","affiliation":[]}],"member":"140","reference":[{"key":"p_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0057647"},{"key":"p_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019211714301"},{"volume-title":"Proceedings of Foundations of Software Science and Computation Structures, ETAPS","year":"1997","author":"Cardelli L.","key":"p_3"},{"volume-title":"No. 1222","year":"1997","author":"Cabri G.","key":"p_4"},{"key":"p_5","first-page":"406","volume-title":"Proceedings of the 7th International Conference on Concurrency Theory (CONCUR'96)","author":"Fournet C.","year":"1997"},{"volume-title":"ObjectSpace Voyager Core Package Technical Overview","year":"1999","author":"Glass G.","key":"p_6"},{"volume-title":"Agent Tcl: A Transportable Agent System. Proceedings of the CIKM Workshop on Intelligent, Information Agents, Fourth International Conference on Information and Knowledge Management (CIKM 95)","year":"1995","author":"Gray R. S.","key":"p_7"},{"key":"p_8","doi-asserted-by":"publisher","DOI":"10.1145\/373243.360215"},{"key":"p_9","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604135"},{"key":"p_10","doi-asserted-by":"publisher","DOI":"10.1023\/B:SUPE.0000026849.98610.e4"},{"key":"p_11","unstructured":"X. Li. Research on the Problems of the Description and the Simulation of Mobile Agents. PhD Thesis,Wuhan University, 2003."},{"key":"p_12","first-page":"1","volume-title":"Logic and Algebra of Specification","author":"Milner R.","year":"1983"},{"issue":"2","key":"p_13","first-page":"239","volume":"3","author":"Misra J.","year":"1995","journal-title":"Journal of Computer and Software Engineering"},{"key":"p_15","doi-asserted-by":"publisher","DOI":"10.1109\/32.666824"},{"key":"p_16","doi-asserted-by":"publisher","DOI":"10.1109\/32.685258"},{"key":"p_17","doi-asserted-by":"publisher","DOI":"10.1023\/A:1012908529306"}],"container-title":["International Journal of Pervasive Computing and Communications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/17427370580000117\/full\/xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.emerald.com\/insight\/content\/doi\/10.1108\/17427370580000117\/full\/html","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,25]],"date-time":"2025-07-25T00:22:14Z","timestamp":1753402934000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.emerald.com\/ijpcc\/article\/1\/2\/115-122\/161192"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,5,1]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,5,1]]}},"alternative-id":["10.1108\/17427370580000117"],"URL":"https:\/\/doi.org\/10.1108\/17427370580000117","relation":{},"ISSN":["1742-7371"],"issn-type":[{"type":"print","value":"1742-7371"}],"subject":[],"published":{"date-parts":[[2005,5,1]]}}}