期刊名称：International Journal of Intelligent Control and Systems
印刷版ISSN：0218-7965
出版年度：2005
卷号：10
期号：2
页码：143-151
出版社：Westing Publishing Co., Fremont
摘要：This paper presents an approach for modeling and model-checking a mobile agent system specified by LAM, which is a two-layer formal method for characterizing logical agent mobility using Predicate/Transition (PrT) nets. Based on the transformation of PrT nets into input programs of the model checker SPIN, we model check a variety of properties with respect to agents, logical agent mobility, agent environments, and system interaction in a mobile agent system model. We demonstrate our approach through a case study on the modeling and analysis of a mobile agent�Cbased clinical information system.
