Formally specifying and verifying mobile agents - Model checking mobility: The MobiOZ approach

被引：0
作者：
Information Systems Architecture Research Division, Grace Center National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101 8430, Japan [1 ]
不详 [2 ]
机构：
[1] Information Systems Architecture Research Division, Grace Center National Institute of Informatics, Chiyoda-ku, Tokyo 101 8430
[2] Computer Science Department, School of Computing, National University of Singapore, Singapore 117543
来源：
International Journal of Agent-Oriented Software Engineering | 2008年 / 2卷 / 04期
关键词：
Formal specifications; Mobile agents; Model checking; Object-Z; SPIN; Verification;
D O I：
10.1504/IJAOSE.2008.020140
中图分类号：
学科分类号：
摘要：
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. © 2008, Inderscience Publishers.
引用
收藏
页码：449 / 474
页数：25
相关论文
共 32 条
  • [1] Bettini L., De Nicola R., Translating strong mobility into weak mobility, Proceedings of 5th International Conference on Mobile Agents (MA) 2001, (2001)
  • [2] Bordini R.H., Fisher M., Pardavila C., Wooldridge M., Model checking AgentSpeak, Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS) 2003, pp. 409-416, (2003)
  • [3] Cardelli L., A language with distributed scope, Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 286-297, (1995)
  • [4] Cardelli L., Gordon A., Mobile agents, LNCS, 1378, pp. 140-155, (1998)
  • [5] Cardelli L., Gordon A., Anytime, anywhere: Modal logics for mobile ambients, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL) '00, pp. 365-377, (2000)
  • [6] Clarke E.M., Grumberg O., Peled D.A., Model Checking, (1999)
  • [7] Cugola G., Ghezzi C., Picco G.P., Vigna G., Analyzing mobile code languages, LNCS, 1222, pp. 93-111, (1997)
  • [8] De Moura L., Owre S., Rueb H., Rushby J., Shankar N., Sorea M., Tiwari A., SAL 2, LNCS, 3114, pp. 496-500, (2004)
  • [9] De Nicola R., Ferrari G., Pugliese R., Locality based Linda: Programming with explicit localities, LNCS, 1214, pp. 712-726, (1997)
  • [10] Derrick J., North S., Simons T., Issues in implementing a model checker for Z, LNCS, 4260, pp. 678-696, (2006)
1234