Int. J. of Agent-Oriented Software Engineering   »   2008 Vol.2, No.4

 

 

Title: Formally specifying and verifying mobile agents – model checking mobility: the MobiOZ approach

 

Author: Kenji Taguchi, Jin Song Dong

 

Addresses:
Information Systems Architecture, Research Division, Grace Center, National Institute of Informatics, 2–1–2 Hitotsubashi, Chiyoda-ku, Tokyo 101–8430, Japan.
Computer Science Department, School of Computing, National University of Singapore, 3 Science Drive 2, Singapore 117543, Singapore

 

Abstract: The notion of the mobile agent has been around for over a decade in order to capture the new form of computation in communication networks. A mobile agent is a computing entity which can move around different hosts on the network, carrying its state and procedures. Mobile Object-Z (MobiOZ), which is designed to provide a practical means to the specifiers who are working on mobile agent applications, is an extended notation of Object-Z, with mobile and communication primitives for specifying and verifying mobile agent applications. In this paper, we will give an overview of the MobiOZ notation and present its semantic foundation, then demonstrate how the specifications in MobiOZ can be simulated and verified by SPIN, a model checker, by translating MobiOZ specifications into PROcess MEta LAnguage (PROMELA), a process-based formal specification language of SPIN.

 

Keywords: mobile agents; formal specifications; Mobile Object-Z; verification; model checking; SPIN; communication networks; agent-based systems; multi-agent systems; MAS.

 

DOI: 10.1504/IJAOSE.2008.020140

 

Int. J. of Agent-Oriented Software Engineering, 2008 Vol.2, No.4, pp.449 - 474

 

Available online: 29 Aug 2008

 

 

Editors Full text accessAccess for SubscribersPurchase this articleComment on this article