Mobility is a network capability with many forms and many uses. Because it is difficult to implement at Internet scale, there is a large and confusing landscape of mobility proposals which cannot easily be compared or composed. "The design space of network mobility" (Pamela Zave and Jennifer Rexford; Recent Advances in Networking, Olivier Bonaventure and Hamed Haddadi, editors, ACM SIGCOMM eBook, August 2013) uses a model of compositional network architecture as an organizing framework to show that there are two fundamental patterns for implementing mobility, and to survey and compare the most important mobility proposals.
The two fundamental patterns for implementing mobility are also important to "Compositional network mobility" (Pamela Zave and Jennifer Rexford; 5th Working Conference on Verified Software: Theories, Tools, and Experiments, Springer-Verlag LNCS 8164, 2014). This paper employs formal modeling and verification to show that different instances of the patterns, used for different purposes in a network architecture, compose without alteration or interference. This result applies to all real implementations that are refinements of the patterns.