This paper presents a formal modeling and simulation framework for mobile agent systems. A Mobile Discrete Event System Specification (MDEVS) formalism is proposed to represent the dynamics of mobile agent systems. The MDEVS formalism supports structural changes of the systems, which include the creation, addition, deletion, and migration of models and the dynamic changes of couplings between models. AgentSim is a software environment for the simulation and execution of mobile agent systems modeled by the MDEVS formalism. AgentSim is implemented as a library built on IBM's Aglets. The modeling and simulation of an e-commerce mobile agent system is exemplified to demonstrate the effectiveness of the proposed modeling framework and the associated simulation environment.