A formalism for hierarchical mobile agents

This paper presents a theoretical and practical framework for constructing and reasoning about mobile agents. The framework is formulated as a process calculus and has two contributions. One of the contributions can model not only individual mobile agents but also a group of mobile agents because the calculus allows more than one mobile agent to be dynamically organized into a single mobile agent. The other contribution can exactly model many features of actual mobile agents, such as mobility and marshaling, which are often ignored in other existing frameworks but may seriously affect the correctness of mobile agents. To demonstrate the utility of the calculus, we constructed a practical mobile agent system whose agents can be naturally and strictly specified and verified in the calculus. The system also offers a security mechanism for mobile agents by using well-defined properties of the calculus