Modelling IP Mobility

Roberto M. Amadio 1 Sanjiva Prasad
1 MEIJE - Concurrency, Synchronization and Real-time Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We study the modelling of {\em mobile hosts} on a network in a simple name-passing process calculus, with the intention of being able to prove properties about a protocol for supporting mobility. Our model may be considered a highly simplified version of proposals for {\em mobility support} in the version 6 of the Internet Protocols (IP). Being fairly general, the model may also apply to mobile software architectures. We believe that such simplified models help in prototyping mobility protocols and reasoning about them while abstracting away excessive details. We concentrate on the issue of ensuring that messages to and from mobile agents are delivered without loss of connectivity. We provide three models of increasingly complex nature of a network of routers and computing agents that are interconnected via the routers: the first is without mobile agents and is treated as a specification for the next two; the second supports mobile agents, and the third additionally allows correspondent agents to {\em cache} the current location of a mobile agent. Following a detailed analysis of the three models to extract invariant properties, we show that the three models are related by a suitable notion of equivalence based on {\em barbed bisimulation}.
Mots-clés : MOBILITY IP
Type de document :
RR-3301, INRIA. 1997
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:40:55
Dernière modification le : samedi 27 janvier 2018 - 01:30:57
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:53:16



  • HAL Id : inria-00073387, version 1



Roberto M. Amadio, Sanjiva Prasad. Modelling IP Mobility. RR-3301, INRIA. 1997. 〈inria-00073387〉



Consultations de la notice


Téléchargements de fichiers