A formal model for mobile agent systems using Z

Summary form only given. This paper proposes a formal definition of a conceptual model for mobile agent systems. This works constitute a part of a general research project aiming at defining a generic interaction model that covers the different facets of the cooperative activity among mobile agent based systems. We propose a framework for the specification of interaction mechanisms among mobile agent systems. Doing so, and using the Z notation, we bring closer the concepts describing a mobile agent systems and the cooperative activity while integrating them with the concepts related to the agent migration. The syntax and the semantic of proposed specifications have been checked using the Z-EVES tool.