Compositional Network Mobility

Abstract

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. This paper presents formal models of two distinct patterns for implementing mobility, explaining their generality and applicability. We also employ formal 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.