Using π-Calculus for Specification of Mobile Agent Communication

G. Jezic and I. Lovrek (Croatia)


Mobile agents, agent communication, formal specification, process algebra, verification.


This paper presents formal specification and verification of agent migration and communication in a mobile agent network. The specification has been written in -calculus process algebra based on link mobility and verified by Mobility Workbench analysis. The model consists of the mobile agents placed at distributed nodes and a mobility management agent responsible for message handling. The specification is focused on remote communication of the agents while migrating through the network. The system has been verified by Workbench model checking features.

Important Links:

Go Back