"The geomorphic view of networking: An abstract model and its uses" is a recent overview talk on this work.
The geomorphic view was first presented in "The geomorphic view of networking: A network model and its uses" (Pamela Zave and Jennifer Rexford; 7th Middleware for Next Generation Internet Computing Workshop, Montreal, Canada, ACM Digital Library, 2012). Here is the workshop talk.
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 the geomorphic view of networking 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. The Alloy and Promela models presented below are appendices to the paper.
The Alloy model of shared state includes the shared state of a hierarchy of network layers, and the effect of mobility events on this state. There are many consistency constraints and other verification conditions in the file, as explained in the paper. Comments in the file document the analyses performed by the Alloy Analyzer.