The mechanisms and design principles needed for achieving optimized handoff for mobile Internet services are poorly understood and need better analysis. This paper contributes to the general theory of optimized handoff and addresses the need for a formal model that can characterize a mobility event and the associated mobility optimization methodologies. It provides a systematic and formal approach to analyzing a mobility fter a thorough analysis of the abstract operations associated with several mobility protocols, it determines that these basic handoff operations form a set of discrete events that can be modeled as Discrete Event Dynamic System (DEDS). It then uses Deterministic Timed Petri nets to model the mobility event and evaluate the performance under different scheduling schemes. This model also helps to validate optimization methodologies that could lead to a set of design principles for any new mobility protocol as well as evaluate its effectiveness.