Abstract
Mobile agents provide an effective and flexible approach to developing complex distributed systems. Formalizing the software architecture of mobile agent systems supports the development of high quality agent systems. In this paper, the software architecture of an interoperable mobile agent system is defined using two-layer predicate transition (PrT) nets. Based on the two-layer PrT net models, a formal model-based approach to develop mobile agents systems is proposed. The approach presented in this paper naturally integrates formal methods and practical approaches in each phase of the development life-cycle of the agent system. The proposed approach for agent systems can also be used to develop other complex software systems.