Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
2000 | 10.1023/A:1008734618526 | Formal Methods in System Design |
Keywords | DocType | Volume |
barbed bisimulation,complex nature,correspondent agent,finite state version,computing agent,modelling,mobile agent,supports mobile agent,internet protocols,detailed analysis,formal methods,protocol analysis,verification,modelling ip mobility,bisimulation,mobility,current location,process description languages,internet protocol | Journal | 17 |
Issue | ISSN | ISBN |
1 | 1572-8102 | 3-540-64896-8 |
Citations | PageRank | References |
5 | 0.55 | 16 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Roberto M. Amadio | 1 | 955 | 94.04 |
Sanjiva Prasad | 2 | 301 | 40.04 |