In: 06, 2006: Proceedings of the Fourth International Workshop on Modelling of Objects, Components and Agents, MOCA'06, Bericht 272, FBI-HH-B-272, pages 201-222. June 06.
Abstract: Mobile systems explore the interplay between locality and connectivity. A subsystem may have a connection to a remote subsystem and use this for communication. It may be necessary or desirable to move the subsystem close to the other in order to communicate. Alternatively, the method of communication may vary depending on proximity. This paper reniews a Petri Net formalisation for mobile systems which is intended to harness the intuitive graphical representation of Petri Nets and the long history of associated analysis techniques. The main contribution of the current paper is to assess the above formalism by using it to model and simulate Mobile IP, an Internet standard which caters for mobile nodes using IP version 4 addresses. These addresses indicate a fixed point of connection to the internet and the protocol caters for nodes being away from home. By defining the model as a Mobile Petri Net, the graphical notation helps to convey the flew of information, and the executable nature of the model opens the way to similation, state space exploration and model checking.