Modelling mobile IP with mobile petri nets

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 reviews 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 attachment 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 flow of information, and the executable nature of the model opens the way to simulation, state space exploration and model checking. © 2009 Springer-Verlag Berlin Heidelberg.