caa a22 4500 475797558 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000801xx s 000 0 eng 10.1023/A:1008734618526 doi (NATIONALLICENCE)springer-10.1023/A:1008734618526 Modelling IP Mobility [Elektronische Daten] [Roberto Amadio, Sanjiva Prasad] We study a highly simplified version of the proposed mobility support in version 6 of Internet Protocols (IP). 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 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 barbed bisimulation. Finally, we report on some experiments in simulating and verifying finite state versions of our model. Kluwer Academic Publishers, 2000 internet protocols nationallicence mobility nationallicence protocol analysis nationallicence formal methods nationallicence modelling nationallicence verification nationallicence process description languages nationallicence bisimulation nationallicence Amadio Roberto Université de Provence, Marseille, France aut Prasad Sanjiva Indian Institute of Technology, Delhi, India aut Formal Methods in System Design Kluwer Academic Publishers 17/1(2000-08-01), 61-99 0925-9856 17:1<61 2000 17 10703 https://doi.org/10.1023/A:1008734618526 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008734618526 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Amadio Roberto Université de Provence, Marseille, France aut NATIONALLICENCE 700 1- Prasad Sanjiva Indian Institute of Technology, Delhi, India aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 17/1(2000-08-01), 61-99 0925-9856 17:1<61 2000 17 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer