Modeling and Analyzing a Mobile Agent-based Clinical Information System

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-based clinical information system.