Focusing on model-driven development for agent-based intelligent systems, a formal semantic model is proposed in this paper. The typed category theory is used to formally describe agent models and their mapping relations, and thus the precise semantic meanings for them are provided. Agent models are described with algebra specifications, and morphisms are used to describe the relationships between agent models, and the morphism types imply the different semantics of agent interactions. The formal semantic model can be used to judge whether a transformation satisfies some property preservation constraints or not, and it can provide an effective support for model-driven agent-based software development. An agent-based intelligent tutoring system is given as a case to illustrate the application of this approach.