The Design Space of Network Mobility

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 to appear, 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.

Compositional Network Mobility

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 to appear, 2013). 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 following formal models are appendices to the paper.

Alloy Model of Shared State

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.

Promela Models of Private Control State

Promela is the language of the model-checker Spin. These models of a point-to-point networked channel include the private control states at each end of the channel, as explained in the paper. Each model includes detailed documentation about what is modeled, what properties it is expected to have, and how Spin was used to verify those properties. There is a sequence of four models, in the following order:

They form a sequence because each model after the first builds on its predecessor. In each subsequent model, new aspects are added. To keep the model simple enough to understand and analyze, some previous aspects-- already well-understood--are removed. A model with different aspects typically has different properties and may require different verification techniques. This sequence of models has significant tutorial value, because it illustrates two important and subtle aspects of model-checking:

Verification employs approximately 16 different modeling techniques and Spin features, some of them very poorly documented. It is easy to run a model checker, but not always easy to understand what the output means. These models can help a student appreciate the relationship between the property to be verified and the technique needed to verify it. These models can also keep students from being misled by the magic of meaningless push-button verification.
When one is trying to apply model-checking to anything real, it is very easy to become frustrated by state explosion. For example, a single model with all the behaviors in this sequence of models would be impossible to verify. This series illustrates how overall behavior can be decomposed and abstracted to get a set of meaningful AND tractable models that achieve the overall goal.