A formal approach to mobility modeling

In the absence of any formal mechanism to analyze the dynamics of handoff systems, it is difficult to predict or verify the systems performance of un-optimized handover or any specific handoff optimization technique. Without an existing mobility system model, it is difficult to design a new customized mobility protocol or design new optimization techniques for an existing mobility protocol in a systematic way. This paper introduces a model of the handover process that identifies the intrinsic operations of a handover event and allows to predict performance for both an un-optimized handover and for specific optimization methodologies under resource constraints. This model also allows to study the behavioral properties of the handoff system such as data dependency and deadlocks. The model-based approach provides the ability to determine the extent of parallelism and proactive operations that are possible among the handoff components.