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 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.
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 LNCS 8164, 2014; the final publication
is available on SpringerLink at link.springer.com).
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
modelchecker Spin.
These models of a pointtopoint 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 wellunderstoodare 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 modelchecking:

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 pushbutton verification.

When one is trying to apply modelchecking 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.