Modeling and simulation of an improved random direction mobility model for wireless networks using colored Petri nets

Abstract

Wireless networks have received increased attention from researchers due to their extensive set of applications and ubiquitous communication facility. The underlying mobility model plays a key role in mobility management, which is a prominent communication means in delivering services to mobile users accurately. Random direction is a synthetic mobility model that is widely used in simulators, while simulation is universally considered the most effective method for the design and analysis of the characteristics of mobility models. However, simulation is limited in its capabilities and it may generate unrealistic, error-prone results and consume more time. Further, the random direction mobility model produces unrealistic movement patterns due to a sharp turn problem and it forces the mobile host to travel to the edge of the terrain. To alleviate the issues of the random direction mobility model, this paper presents a colored Petri net (CPN)-based formal approach as an improved direction mobility model. Further, the proposed algorithm to tackle the sharp turn problem is implemented by using the CPN formalism. The formal semantics of the CPN allow a graphical, intuitive approach to design, simulate, execute, and validate the model.

Keywords

Wireless networks mobility models colored Petri nets formal methods random direction mobility model

1. Introduction

Conventionally, simulation is the most effective way to design and validate the performance of a developed model. The major role of a mobility model is to generate movement patterns according to real-life scenarios in simulation-based studies. Numerous mobility models offering diverse characteristics are employed in simulation-supported research. Some models are simplistic and others are based on a comprehensive modeling approach to generate more realistic traveling patterns. The accuracy of a mobility model is highly dependent on the degree of realism. A precise and realistic mobility model generates more accurate simulation results to evaluate network parameters.

Wireless networks are part of our daily life; recent developments in the field of short-range radio technology have led to renewed interest in wireless mesh networks (WMNs).¹ WMNs necessitate improved mobility management with higher data rate and wider coverage to support mobile clients roaming around the network. WMNs offer easy deployment and seamless connectivity to mobile users and the question of how to provide seamless mobility is a driving force behind research. Mobility management plays a crucial role in the delivery of services to roaming users with mobile terminals. The underlying mobility model generates the trajectories of the mobile host (MH) or simple station (STA) and has a major influence on the design and performance of the developed system. A mobility model should incorporate important features that influence the characteristics of an STA.

Mobility models can be divided into seven broad categories: (i) individual mobility models; (ii) group mobility models; (iii) flocking mobility; (iv) autoregressive mobility models; (v) non-recurrent mobility; (vi) virtual game-driven mobility; and (vii) time-variant community mobility.² Mobility patterns are the main criteria and key determinants that influence the performance of the network. Movement patterns can be extracted as traces from mobility models. Trace-base mobility models use traveling patterns based on a deterministic approach as well as observations from real-life scenarios. The characteristics of the model are obtained by monitoring the movement patterns of users carrying mobile devices.

Synthetic mobility models attempt to model the mobility of each MH in a simplistic manner based on its direction, speed, transition time between home and destination, length between two points, and the distribution of MH positions. The random direction mobility model is a synthetic-based model which falls under the individual mobility model category and is very similar to the random waypoint (RWP) model.^3,4 This model forces a MH to travel to the edge of the terrain. A host randomly chooses a direction from (0, 2π) and moves; after completing one epoch it changes direction and speed and continues moving until the simulation is finished. Some performance-related issues of the random direction mobility model have been identified in the literature.^5,6 The model produces unrealistic movement patterns due to a sharp turn problem. Such behavior is depicted in Figure 1, which reflects an unrealistic short turn at the end of each epoch. In our modified model, we present for the first time an improved random direction mobility model (IRDMM) by eliminating the short turn issue to produce more realistic traveling patterns based on a formal approach, i.e., colored Petri nets.

Figure 1.

Traveling pattern of a MH using the random direction mobility model.⁶

Traditionally, simulation is the standard tool for conducting wireless networks research and has many benefits. However, the literature demonstrates that newcomer students and researchers in this area often become perplexed by the complexity of simulators and lose their concentration on research.⁷ Formal methods are mathematical-based techniques that have great potential and are proven to be a powerful tool for investigation of the correctness of a model’s properties.⁸ The choice of formal modeling approach is usually motivated by its power to study, to detect inconsistency, and to reduce the “time to market.” Moreover, formal methods have rigorous computer-based tool support, which checks all possible execution paths throughout the system and reveals virulent concurrent errors that have not been unveiled by implementing other testing methods.

Colored Petri nets (CPNs) are formal methods suitable for development of concurrent and complex models.^9,10 Many techniques, i.e., timed token colors, hierarchical modeling, recursive functions, and markup language, to model control flow and data constraints are used to facilitate modeling complex systems. CPNs combine Petri nets and the functional programming language Standard ML (SML).^11,12 CPN Tools,¹³ which is a powerful software for modeling and analysis of CPN models, is widely accepted and adopted in many significant projects by the research community.

A significant contribution presented in this paper could be summarized into two phases. First, a CPN-based formal model of an IRDMM is proposed. In addition, a two-dimensional (100 × 100 m²) terrain is established for simulation purposes and to develop a CPN-based IRDMM. Second, a detailed algorithm, which is proposed to handle the sharp turn problem, is implemented through a CPN in the proposed mobility model. We validate the model to verify some functional properties of the developed model by using extensive simulation and state space analysis techniques. The proposed model provides a basis for evaluating the performance of protocols through CPNs.

The rest of the paper is organized as follows. Section 2 describes the related work in this domain. Section 3 presents preliminaries about Petri nets while Section 4 describes a brief introduction to the traditional random direction mobility model. Section 5 presents the formal modeling of an IRDMM by using CPN tools. Section 6 describes state space analysis of the model and verification results. Finally, Section 7 contains the conclusions and summarizes our achievement.

2. Related work

In evaluation of the performance of wireless networks, the movement patterns of the mobility model play a vital role. The literature reflects that very few publications can be found that address the mobility issues in a wireless network by using CPNs. The work of Kristensen et al. can be considered as a landmark in CPN-based modeling.¹⁴ They abstractly described both micro and macro mobility architecture scenarios in ad-hoc networks. Their main focus was to develop a model through integration of routing protocols of conventional networks with routing protocols of ad-hoc networks. A valuable contribution of their work is that the CPN model reflects communication and mobility properties in a single model. The model is most appropriate for mobility test cases. Xiong et al. studied mobility in Ad-Hoc Networks and suggested a topology approximation (TA) structure to overcome the dynamically changing topology problem.¹⁵ They implemented their proposed mechanism to build a CPN model based on an ad hoc on demand distance vector (AODV) routing protocol. The results showed that the TA mechanism exhibits realistic movement characteristics and is able to mimic the dynamic changes of network topology.

Capturing mobility patterns through a CPN is a most challenging activity. Khan et al. presented a CPN-based formal model of the well-known random walk mobility model for WMNs without border effect and speed decay problems.¹⁶ The model is more appropriate for generating different mobility patterns; these patterns can further be used for analyzing the performance of routing protocols and mobility management in wireless communication networks. The proposed model can be easily modified to generate complex mobility patterns. An elegant CPN-based synthetic RWP mobility model was presented by Agrahari and Chinara.¹⁷ However, despite their contribution there are some shortcomings, as this model is not able to generate the trace patterns of every epoch. In order to produce more realistic movement patterns a novel modification was made by Resta and Santi by removing the border effect issue from the RWP mobility model.¹⁸ The spatial distribution generated by their developed model is different from the standard model. Further, Khan et al. also presented a CPN-based executable specification and verification of the classical RWP mobility model.¹⁹ The proposed formal approach improved the RWP mobility model by removing the “border effect” and resolved the “speed decay” problem. An accurate and extendable community-based WMN CPN formal model was proposed by Khan et al.,²⁰ where a mobile node can randomly move as well as send data packets to other MHs. The model concentrates on mobility requirements and systematically verifies WMN environment. To eradicate broad criticism of the RWP recently, we proposed SHER (“show home and exclusive regions”),²¹ a magnificent random mobility model that focuses on social interaction of a user. The model perceives a MH’s history of visits to different locations and yields five hotspots. The formal model removes six integral problems of random models, i.e., sudden stops, memory less movements, the border effect, temporal dependency of velocity, pause time dependency, and speed decay in a single model. These trajectories can be used to predict the next itinerary of a mobile user, which will improve the performance of wireless communication networks. It has been found in the literature that not much work has been done on using CPNs on mobility issues for wireless networks and that it could add benefits towards simulation modeling for wireless networks.

3. Preliminaries about Petri nets

In this section, we present some basic concepts and behavioral properties of Petri nets and colored Petri nets that are used to verify the dynamic behavior and correctness of the proposed algorithm. We suppose that readers of this paper are familiar with colored Petri nets; otherwise readers are referred to Jensen.⁹ The formal definitions of both are given below.

Definition 1 (Petri net):¹¹ A Petri net $(N, M_{0})$ is a net PN with five tuples $(P, T, F, W, M)$ where

P is a finite set of places and T is a finite set of transitions $such that P \cap^{T} = \emptyset and P \cup^{T} \neq \emptyset;$

F is the flow relation (set of arcs) between places and transitions $such that F \subseteq (P \times T) \cup (T \times P);$

W is a weight function that maps a positive number to a set of flow relations such that W = F→ {1, 2, 3…} is the number of arcs associated with places and transitions;

M is a function that maps non negative integers to set of places such that $M : P \to N$ and M(p) represents the number of tokens in any place and $M_{0}$ is called the initial marking of the net.

Definition 2 (colored Petri nets (CPN) and hierarchical CPN):⁹ A colored Petri net is a tuple CPN = (Σ, P, T, F, V, C, G, E, I) where

Σ is the finite set of data types, also called a color set (i.e., it is the same as programming types), which determines the data values and functions that can be used in guards, arc expressions, and during initialization;

P is a finite set of places and T is a finite set of transitions $such that P \cap T = \emptyset and P \cup T \neq \emptyset;$

F is a finite set of arcs $such that P \cap T = P \cap F = T \cap F = \emptyset$ ;

V is a node function $such that V : F \to (P * T) \cup (T * P)$ ;

C is a color mapping that maps data types to sets of places such that C : P →Σ.

The color function C maps each place p to a type C(p), which means that each token on p must have a data value that belongs to C(p).

G is a guard function which is defined from set T into the expressions such that $\forall t \in T :$ Type $(G (t)$ Boolean and Type $(Var (G (t))) \sum$

which means for any transitions $t \in T$ , the guard of t is a Boolean expression, where all variables have types from Σ.

E is an arc expression function that is defined from F into expressions such that ∀ a $\in F \in Type (E (a)) = C {(p)}_{Ms}$ and $Type (Var (E (a)) \sum$ where p is a place of $V (a)$ .

which means for any arc $a \in F$ , the type of E(a) is the multiset $C {(p)}_{Ms}$ , which means that E(a) must evaluate to multisets over the type of the adjacent place p. Moreover, all variables in an arc expression E(a) have a type in Σ.

I is the initialization function . It is defined from set P into closed expression such that $\forall p \in P : Type (I (p)) = C {(p)}_{Ms} .$

I map seach place $p \in P$ into a closed expression that must be of type of C ${(p)}_{Ms} .$

Further, a hierarchical CPN is a four-tuple, i.e., CPN_H = (S, SM, PS, FS), where S is a finite set of modules. Each module is a CPN module. SM is a submodule function that assigns a submodule to each substitution transition. It is required that the module hierarchy is acyclic. PS is a port–socket relation function that assigns a port–socket relation to each substitution transition t and FS is a set of non-empty fusion sets.

Definition 3 (reachability):¹¹ A marking $M_{k}$ is said to be reachable from marking $M_{0}$ if there exists a sequence $σ$ of transition firings that transforms $M_{0}$ into $M_{k}$ . When $M_{k}$ is reachable from $M_{0}$ by $σ$ , we write $M_{0} [σ > M_{k}]$ .

Definition 4 (boundedness and safeness):¹¹ For all $p_{i} \in P of PN (N, M_{0})$ , PN said to be b-bounded if $\forall M_{k} \in R (M_{0}) : M_{k} (p_{i}) \leq b$ and PN is said to be safe if $M_{k} (p_{i}) \leq 1$

Definition 5 (deadlock and deadlock free):¹¹ A transition $t_{j} \in T$ is said to be dead transition at marking $M_{k} \in R (M_{0})$ , if there is no reachable marking to make transition $t_{j}$ enabled. A marking $M_{k} \in R (M_{0})$ is said to be a deadlock if $\forall t_{j} \in T$ , $t_{j}$ is dead. A PN (N, M₀) is said to be deadlock-free if and only if there is no deadlock.

Definition 6 (liveness):¹¹ A transition $t_{j} \in T$ is said to be live if and only if there is a marking $M_{k}^{'}$ reachable from each $M_{k} \in R (M_{0})$ such that $M_{k}^{'}$ enables $t_{j}$ and PN $(N, M_{0})$ is live if $\forall t_{j} \in T$ : $t_{j}$ is live.

4. Theory of random direction mobility model

The synthetic random direction model was proposed by Royer et al. to eliminate the density wave phenomenon of the RWP mobility model and is widely used in network simulation.³ A density wave is the clustering of a MH in one part of a communication region. In this model, each mobile node is independent; first every node selects an angle between 0 and 359° and finds a destination on the boundary of terrain in the selected direction. After that, a MH randomly selects speed to travel. Upon completing the epoch, the MH pauses for a certain period. After resting for pause time, the host again decides a new direction and speed and travels to complete a second movement epoch up to the boundary. The above process is independently repeated again and again until the simulation is accomplished. Although remarkable efforts were made by Royer et al. to overcome the density wave problem in the RWP model,³ but as reflected in several studies,^2,5,6 such random models still suffer from the short turn problem. The movement pattern of a MH employing sharp turn behavior can be seen in Figure 1.

5. CPN-based modeling for the improved random direction mobility model

5.1 Environment scenario

An improved random direction timed-based hierarchical CPN mobility model consists of five modules (pages), the top level scenarios module is presented in Figure 2. The model has a dynamic nature, so MH [N¹…Nⁿ] can be randomly spread in a 100 × 100 m² communication area. A desired number of MHs can be introduced in the proposed model. A MH can select a random angle and therefore it can be in any one of four quadrants. The model contains a finite set of places P, a finite set of transitions T, a set of directed arcs A, a finite set of non-empty color sets Σ, a finite set of typed variables V, a color set function C, that assigns a color set to each place, a guard function G, an arc expression function E, that assigns an arc expression to each place, and an initialization function I. The most abstract scenarios module has one substitution transition ImprovedRandomDirectionModel, as indicated by the associated HS-tag, and two places ND and BBONE with color sets NO and RDMOVE1, as shown in Figure 2.

Figure 2.

The scenarios page – top level CPN model module in the initial marking M₀.

The color sets are defined using basic SML types. The Val (constant) tn (total nodes) is globally declared as 1; it specifies the dynamics of the model and a user can enhance the value up to any desired number of nodes. The color set RCOOR (real coordinates) is defined as product color set of simple color set RCOR by using the color set constructor product. The RDMOVE1 is a timed eight-tuple color set, consisting of node ID, step number, home coordinates, current coordinates, slope, speed, and current step number (Figure 3).

Figure 3.

Declaration of color set for scenarios page.

Figure 4 shows a graphical representation of the module hierarchy for the developed CPN model. The hierarchy page depicts an overview of modules and their relationship. The proposed model contains a finite set S of modules and each module $s \in S$ is defined as s = ( $CP N^{s}$ , $P_{port}^{s}$ , $T_{sub}^{s}$ , $P T^{s}$ ). In our proposed model we have following five sets of modules:

S = {SCENARIOS, IRDIR, HOME, MOBILITY, SMOOTH}

Figure 4.

Hierarchical view of the improved random direction mobility model.

The element $T_{sub}$ enables the union of all substitution transitions. Each substitution transition t is mapped through the submodule function SM. The proposed model contains the following:

\begin{array}{l} T_{sub} = {{ImprovedRandomDirectionModel}^{SCENARIOS}, {HOME}^{IRDIR}, {MOBILITY}^{IRDIR}, {Smooth Turn}^{MOBILITY}} \\ S M : {\begin{matrix} {ImprovedRandomDirectionModel}^{SCENARIOS} : & IRDIR \\ {HOME}^{IRDIR} : & HOME \\ {MOBILITY}^{IRDIR} : & MOBILITY \\ {SmoothTurn}^{MOBILITY} : & SMOOTH \end{matrix} \end{array}

The Scenarios page contains the module IRDIR. The IRDIR module and its two submodules HOME and MOBILITY are responsible to model the operations of the IRDMM. The module HOME develops the first trajectory, which contains a mobile node ID, i.e., MH ID, step number, home coordinates, and angle towards the destination. The MOBILITY module represents a movement pattern of MH, while its submodule SMOOTH generates sharp turns on completion of every epoch.

5.2 Hierarchical pages of CPN Model

The hierarchical IRDIR page is depicted in Figure 5, which corresponds to the IRDIR#2 node given in Figure 4. The IRDIR module is used to tie up MOBILITY and HOME modules and it creates interface to SCENARIO page. The module contains three transitions and four places. The rectangles HOME and MOBILITY are substitution transition, while FRAM is an ordinary transition, as indicated HS-tag positioned next to them. Place ND is an input socket port $P_{sock}^{in} (t)$ , while place BBONE is an output socket port $P_{sock}^{out} (t)$ . These places constitute interface to connect IRDIR page with other modules to exchange tokens. For the SCENARIO module in Figure 2 and the substitution transition ImprovedRandomDirectionModel we have:

\begin{matrix} P_{sock}^{in} (IRDIR) = {ND} \\ P_{sock}^{out} (IRDIR) = {BBONE} \end{matrix}

Figure 5.

The IRDIR module in the initial marking M₀.

The current topology is represented by one token at place ND, which shows that one mobile node (MH) is ready to move at time 0. The definitions of color sets STA_HOME and GO are given in Figure 6.

Figure 6.

Declaration of color set for GO and STA_HOME.

The substitution transition HOME generates the MH for participation, while MOBILITY is responsible to model traveling patterns. Transition FRAM has one input arc and one output arc, it models payload and sends to place RDIR-RDY (random direction ready), which has the type GO. The following binding is an example of frame token sent to place RDIR-RDY:

After firing transition FRAM, following nine-tuple token moves to the place RDIR-RDY:

RDIR-RDY→1′((“MH-1”,6),1,[(26.0,100.0)],[(26.0,100.0)],291.0,1,1,1.0,START)@11

Figure 7 depicts the HOME page, which enables the CPN model to generate MHs for simulation. The module contains four places and two ordinary transitions. The place ND in this module is called port place and represents the total number of MHs. Place ND is an input socket port $P_{sock}^{in} (t)$ , while place STA_HOM1 is an output socket port $P_{sock}^{out} (t)$ .

\begin{matrix} P_{sock}^{in} (HOME) & = {ND} \\ P_{sock}^{out} (HOME) & = {STA_HOM 1} \\ P & = {MH, St - Time} \\ T & = {TimeOfArival, START} \end{matrix}

Figure 7.

The HOME page in the initial marking M₀.

The transition TimeOfArrival models mobile node with arrival time. The following binding is an example of a node with arrival time sent to place MH:

After firing transition TimeOfArrival, the following two-tuple token is moved to the place MH, which has a NODE color set. The function NewMH takes two inputs host ID and arrival time and produces the following token of NODE type:

MH→1′(“MH-1”,6)@6

Figure 8 illustrates page MOBILITY, which is responsible for mobility management of MHs. The page has two ordinary places, two output socket places $P_{sock}^{out} (t)$ , one input/output socket place $P_{sock}^{i / o} (t)$ , and two transitions, one ordinary and one substitution, as noted below:

\begin{matrix} P_{sock}^{out} (MOBILITY) & = {BBONE, STA_HOM 1} \\ P_{sock}^{i / o} (MOBILITY) & = {RDIR_RDY} \\ T_{sub} & = {SmoothTur n^{MOBILITY}} \\ P & = {CRdntChkr, CRVE} \\ T & = {MOVE} \end{matrix}

Figure 8.

The MOBILITY module.

The MOVE transition in Figure 8 is most important in the model; it has one input and four output arc expressions. Important functions implemented by MOVE transition are:

fun CRNDTCHKR (z2:LCOOR,id:NODE, s:STATUS)
This function is used to check quadrant of current coordinates.

fun BCHKR(z2:LCOOR,c2:REAL,s:STATUS)
This boundary checker function is used to limit MH to travel within terrain.

fun MOVE (id, cstps, home, crunt, slop, maxsp, csp, cntr)
The MOVE function is used to restrict MH to move to next coordinate after satisfying all imposed conditions.

fun xaxis (x:LCOOR, a:REAL, c:REAL)
Generates next x-axis according to parametric equation formula x = r cos(t)

fun yaxis (x:LCOOR, a:REAL, c:REAL)
Generates next y-axis according to parametric equation formula y = r sin(t)

When a MOVE transition occurs, it fetches one token from input place RDIR_RDY with input arc expression (id,cstps,home,crunt,slop,maxsp,csp,cntr,status). The variables of incoming arc expression are declared as:

var slop	:	RCOR;	( The itinerary angle of movement )
var maxsp,csp,cstps	:	INT;	( The integers are used to describe maximum speed, current speed, current step number )
var home,crunt	:	LCOOR;	( The home, current coordinates of MH )
var id	:	NODE;	( The Identity Number of MH )
var status	:	STATUS;	( The current status of MH )

The transition MOVE bound to following binding and after firing token sent to the place RDIR_RDY.

<slop=292.0,cstps=1,current=[(26.0,100.0)],maxsp=1,cntr=1.0,csp=1, id=(“MH-1”,6),home=[(26.0,100.0)],status= START>

The following arc expression is implemented on outgoing arc from the transition MOVE to the place RDIR_RDY:

if BCHKR(crunt,cntr,status) then 1′ MOVE(id,cstps,home,crunt,slop,maxsp,csp,cntr)else empty

If the above condition is satisfied then following nine-tuple token moves back to the place RDIR_RDY after increasing one step to next coordinate:

1′((“MH-1”,6),2,[(26.0,100.0)],[(26.37,99.07)],292.0,1,1,2.0,START)@17

The substitution transition SmoothTurn corresponds to the modeling of smooth curve. Figure 9 shows the SMOOTH module, which enables the CPN to draw an actual curve when MH finishes its itinerary. The page has two ordinary places, one input socket place $P_{sock}^{in} (t)$ , two output socket places $P_{sock}^{out} (t)$ , one input/output socket place $P_{sock}^{i / o} (t)$ , and two ordinary transitions, as mentioned below:

\begin{matrix} P_{sock}^{in} (SMOOTH) & = {CRVE} \\ P_{sock}^{out} (SMOOTH) & = {BBONE, STA_HOM 1} \\ P_{sock}^{i / o} (SMOOTH) & = {CRdntChkr} \\ P & = {TURN, CrvCntr} \\ T & = {NOWCURVE, SMOOTH} \end{matrix}

Figure 9.

The SMOOTH module.

The place CRdntChkr (quadrant checker) keeps track the current quadrant of the MH. A MH can be in any one of four quadrants, i.e., Quadrant-I (0–90°), Quadrant-II (90–180°), Quadrant-III (180–270°), and Quadrant-IV (270–360°). The place CrvCntr (curve counter) is used to model the incremental counter to draw a curve. The place BBONE (back bone) keeps complete information about every step of MH. The place TURN models actual curve through input arc expression. After completing the curve, a token having update status is sent to place STA_HOM1, where circle repeats and MH selects new epoch for traveling. The transition NOWCURVE fetches three tokens from input places CRdntChr, CrvCntr, and TURN and produces back a curved eight-tuple coordinate’s token to place TURN. The curved process repeats, until complete curved coordinates are updated at place TURN. The procedure to decide the next grid based curve coordinate is shown in Algorithm I.

Algorithm I :

Remove sharp turn

Input:

C_{cordnt}

, Current quadrant of MH

C_{crvcntr}

, Curve Counter

I_{id}

, Identity of MH

C_{cstps}

, Current step number of MH

H_{ij}

, Home grid coordinates of MH

C_{xy}

, Current grid coordinates of MH

S_{slop}

, Moving angle of itinerary

S_{maxsp}

, Maximum speed

S_{csp}

, Current speed

C_{cntr}

, Global counter

Output

C_{Turn}

, Curve grid coordinates of next cell

C_{crvcntr}

, Increment in curve counter

B_{Bbon}

, Updates current curved gird coordinates to back bone

N_{Sthm}

, After completion curve, update information for new epoch

crvcntr < 6

while TRUE do

1′(id,cstps+1,

[cordnt == 3

While TRUE do

(crvcntr == 1 -> x+ 4) & (crvcntr == 2 -> x+ 2) & (crvcntr == 3 -> x)

& (crvcntr == 4 -> x − 2) & (crvcntr == 5 -> x− 4)

end

cordnt == 1

While TRUE do

(crvcntr == 1 -> x− 4) & (crvcntr == 2 -> x−2) & (crvcntr == 3 -> x)

& (crvcntr == 4 -> x+ 2) & (crvcntr == 5 -> x+ 4)

end

else

(i < 50 -> x+ 1) & (~i -> x− 1)

end

cordnt == 2

While TRUE do

(crvcntr == 1 -> y− 4) & (crvcntr == 2 -> y− 2) & (crvcntr == 3 -> y)

& (crvcntr == 4 -> y+ 2) & (crvcntr == 5 -> y+ 4)

end

cordnt == 4

(crvcntr == 1 -> y + 4) & (crvcntr == 2 -> y + 2) & (crvcntr == 3 -> y)

& (crvcntr == 4 -> y− 2) & (crvcntr == 5 -> y− 4)

end

else

(j < 50 -> y+ 1) & (~j -> y− 1)

end ]

, slop,maxsp,csp,cntr+1

else

empty

5.3 The traveling sequence of a mobile host

As the simulation starts, the only enabled transition of the developed CPN model is TimeOfArival at page HOME. The place ND produces the desired number of MHs to participate in the simulation process. Transition TimeOfArival generates a two-tuple token representing MH-ID with arrival time, i.e., < 1′(“MH-1”,9)@9 >. The place MH receives a token from transition TimeOfArival and enables transition START, which is responsible to produce a five-tuple token representing MH-ID, step number, Home grid coordinates, and angle to move, i.e., <1′((“MH-1”,9),1,[(26.0,100.0)],292.0)@9>. The place STA_HOM1, which is a port-socket place between HOME and IRDIR pages, captures a token form the START transition and enables transition FRAM on page IRDIR. When transition FRAM occurs it produces the following nine-tuple token to the place RDIR_RDY:

<1′((“MH-1”,9),1,[(26.0,100.0)],[(26.0,100.0)],292.0,1,1,1.0,START)@19>

Place RDIR_RDY is an input/output socket for the substitution transition MOBILITY. Now transition MOVE on submodule MOBILITY is enabled by firing transition FRAM on the IRDIR page. The transition MOVE has one input and four output arcs. The MOVE transition is responsible for generating the MH at each step according to random direction mobility model specifications. The MOVE transition remains enabled on each fire and produces an updated token back to the place RDIR_RDY until the MH reaches the boundary of the communication region. After completion of the first epoch, the transition SMOOTH at page SMOOTH is enabled, which has one input and two output arcs. When transition SMOOTH occurs, it adds tokens to the places CrvCnter and TURN and also enables transition NOWCURVE. When transition NOWCURVE occurs after satisfying all enabled bindings it will remove a multiple set of tokens from CRdntchkr, CrvCntr, and TURN places and add a curved coordinate multi-set token to the place TURN after the evaluation arc expression, as per sharp turn Algorithm I. The transition NOWCURVE continues to repeat, occurring until the curve process finishes according to the specified algorithm. Figure 10 shows part of the final simulation output, where a movement pattern of a single MH is illustrated after removing the sharp turn problem.

Figure 10.

The traveling pattern of a single MH without sharp turn problem.

The NOWCUVE transition sends a token with new destination for the second epoch to the output socket place STA_HOME1 after completion of the first epoch with curved coordinates. The output socket place STA_HOM1 enables the FRAM transition on the IRDIR page, which generates a token for the RDIR_RDY place and the loop process is repeated again until the simulation stops. The BBONE place is responsible for recording the complete information of every step of the MHs during simulation. Figure 11 illustrates the scenario page after 2500 steps with time stamp 142. The top page is showing 20 nodes, MH-1 to MH-20, completed epochs are 40, and at the BACK BONE place there are 2400 tokens, showing individual movement patterns of each MH.

Figure 11.

The traveling pattern of 20 MHs based on improved random direction mobility model.

6. Simulation analysis and discussion

In order to simulate and verify the IRDMM we used the CPN Tool. Through state space analysis we can analyze all the standard properties of the model, such as boundedness, reachability, liveness, home, and fairness. In order to retain simplicity and ease of monitoring of the behavior of the developed model as well as movement patterns, the state space tool’s options are fixed to partially generate only 500 nodes. Table 1, which shows the state space standard report for movement of one MH and statistics, reveals that the O-graph (occurrence graph) has 501 nodes and 500 arcs. Strongly connected graphs (SCG) exist, so the model has infinite occurrence sequences and may not terminate. An MH can move in the communication range without any restriction.

Table 1.

State space report.

Statistics
----------------------------------------------------------------
State Space
Nodes: 501
Arcs: 500
Secs: 5
Status: Partial
Scc Graph
Nodes: 501
Arcs: 500
Secs: 0
Boundedness Properties
----------------------------------------------------------------
Best Integer Bounds
	Upper	Lower
HOME’MH 1	1	0
HOME’St 1	1	1
IRDIR’RDIR_RDY 1	1	0
IRDIR’STA__HOM1 1	1	0
MOBILITY’CRVE 1	1	0
MOBILITY’CRdnt_Chkr 1	1	0
SCENARIOS’BBONE 1	483	0
SCENARIOS’ND 1	1	0
SMOOTH’Crv_Cntr 1	0	0
SMOOTH’TURN 1	0	0
Best Upper Multi-set Bounds
IRDIR’STA__HOM1	1	1′((“MH-1”,9),1,[(32.0,100.0)],284.0)
MOBILITY’CRVE	1	1′((“MH”,9),98,[(32.0,100.0)],
		[(55.466,5.881)],284.0,1,1,98.0)
MOBILITY’CRdnt_Chkr	1	1′((“MH-1”,9),2)
SCENARIOS’BBONE	1	1′((“MH-1”,9),1,[(32.0,100.0)],
		[(32.0,100.0)],284.0,1,1,1.0)++
		1′((“MH-1”,9),2,[(32.0,100.0)],
		[(32.241,99.029)],284.0,1,1,2.0)++
		1′((“MH-1”,9),3,[(32.0,100.0)],
		[(32.483,98.059)],284.0,1,1,3.0)++…continue…
SCENARIOS’ND	1	1′1
SMOOTH’Crv_Cntr	1	empty
SMOOTH’TURN	1	empty
Best Lower Multi-set Bounds
HOME’MH	1	empty
HOME’St	1	1′9
IRDIR’RDIR_RDY	1	empty
IRDIR’STA__HOM1	1	empty
MOBILITY’CRVE	1	empty
MOBILITY’CRdnt_Chkr	1	empty
SCENARIOS’BBONE	1	empty
SCENARIOS’ND	1	empty
SMOOTH’Crv_Cntr	1	empty
SMOOTH’TURN	1	empty
Home Properties
---------------------------------------------------------------
Home Markings
Initial Marking is not a home marking
Liveness Properties
---------------------------------------------------------------
Dead Markings
[501]
Dead Transition Instances
SMOOTH’NOW_CURVE 1
SMOOTH’SMOOTH 1
Live Transition Instances
None
Fairness Properties
---------------------------------------------------------------
No infinite occurrence sequences.

6.1 Boundedness properties

Upper and lower bounds properties specify the maximum and minimum number of tokens that can reside on a specific place in any reachable marking. It is important to determine whether the proposed model prevents overflow. A net is said to be a k-bounded if any place contains less than or equal to k tokens, while k is any non-negative integer. If a place contains more than k tokens then it is unbounded. If k is equal to one (1-bounded), then this net is safe. The CPN model has 10 places and seven transitions. The six places HOME’MH, HOME’St, IRDIR’RDIR_RDY, IRDIR’STA__HOM1, MOBILITY’CRVE, MOBILITY’CRdnt_Chkr, SCENARIOS’ND, SMOOTH’Crv_Cntr, and SMOOTH’TURN have one best upper integer bound (1-bounded), so its mean developed model is safe. The place SCENARIOS’BBONE is unbounded and has a best upper integer bound of 483. Actually, BBONE place is a monitoring place which keeps track of every step. If we remove this place, there will be no effect on the model’s execution and performance. Figure 8 shows only input arcs of BBONE place.

6.2 Deadlock freedom

A highly prominent property is whether a CPN model is deadlock free, which means that its mean model should not reach a terminal state. The terminal state specifies that there no transition is enabled for further execution. Our proposed model is deadlock free. The state space report in Table 1 specifies that marking 501 is dead marking. The sentiment about 501 dead marking is that it is the dead marking of Petri nets but not the model as we fixed options of state space tool to generate state space report up to 500 nodes for the purpose of simplicity. Figure 12 illustrates the non-terminating behavior of the proposed CPN IRDIR mobility model. The following query also verifies deadlock freedom:

Figure 12.

Acyclic non-terminating behavior of the CPN model.

6.3 Terminating behavior

Another important property for verification is whether the developed model is terminating or not. A terminating state specifies a marking where no further transition is enabled or the model has finite runs. The proposed CPN IRDMM has infinite runs, so it is not terminating because the model has an acyclic structural behavior. Figure 12 shows part of the flat version of the proposed CPN model, where bold places, transitions, and arcs verify the acyclic non-terminating property of the IRDIR mobility model.

6.4 Dead transition

A transition t is said to be a dead transition in the marking m if it can never become enabled in any reachable marking m₀ during execution. This means that every transition should occur at least once on every run. Our proposed model does not have any dead transitions. This can be verified by implementing the following query which shows an empty list:

6.5 Liveness

The liveness property is stronger than absence of dead transition. This property specifies that a transition t can be enabled again during execution of the model. The proposed IRDIR mobility model is partially live, as depicted in Figure 12.

6.6 Home-marking

The liveness property ensures that a transition t can always be fired again, in the same way that a home property specifies that a marking m can always be reached again during execution of the model. The proposed IRDIR mobility model has partial home-marking, as presented in Figure 12.

7. Conclusion

The main role of a mobility model is to closely emulate real-life scenarios. Several mobility models with different characteristics are employed in simulation research. To our knowledge, an improved random direction mobility model has been presented for the first time by using colored Petri nets. As stated in Section 1, the research was carried out to remove a sharp turn problem from the random direction mobility model. In this paper, a timed-hierarchical CPN model has been developed with smooth curved turns. Most of the existing mobility research is based on a NS-2 simulator. We envisage that our work will open a new paradigm of research based on formal modeling. An accurate and dynamic executable IRDIR mobility model is able to capture the qualitative features of mobile nodes. Extensive simulation experiments were conducted in order to verify the validity of the proposed model. The model is more appropriate for generating different mobility patterns. These patterns can be further implemented for removing the mobility management performance issues in wireless communication networks. The model can be easily modified and extended to capture complex scenarios. There are several directions for future work; a more compact mobility model with tokens representing obstacles could be developed. Further research would be devoted to develop more realistic mobility models.

Footnotes

Funding

This research received no specific grant from any funding agency in the public, commercial, or not-for-profit sectors.

Author biographies

Naeem Akhtar Khan received an MS degree in computer science from the University of Agriculture, Faisalabad, Pakistan in 2008. He is currently studying for his PhD with the Faculty of Information Technology at the University of Central Punjab in Lahore, Pakistan. His research interests include the fourth generation wireless networks, mobility management and formal methods (colored Petri Nets).

Farooq Ahmad is an associate professor in the Department of Computer Science at the COMSATS Institute of Information Technology in Lahore, Pakistan. He received his PhD degree in Computer Science from Harbin Institute of Technology in China. He has numerous publications in reputed international journals. He was the vice-chair of IEEE Computer Society Lahore Section from 2011 to 2012. He was a conference co-chair and an invited speaker in several national and international conferences. His research interests are formal modeling, verification, and simulation and Petri net theory and applications.

References

Akyildiz

Wang

Wireless mesh networks: a survey. Comput Networks 2005; 47: 445–487.

Roy

. Handbook of mobile ad hoc networks for mobility models. New York, NY, USA: Springer Science & Business Media, 2010.

Royer

Melliar-Smith

Moser

LE.

An analysis of the optimum node density for ad hoc mobile networks. In IEEE international conference on communications, 2001 (ICC 2001), vol. 3, pp.857–861. IEEE, 2001.

Johnson

Maltz

DA.

Dynamic source routing in ad hoc wireless networks. In Mobile computing. New York: Springer US, 1996, pp.153–181.

Pazand

McDonald

A critique of mobility models for wireless network simulation. In 6th IEEE/ACIS international conference on computer and information science, 2007 (ICIS 2007), pp.141–146. IEEE, 2007.

Camp

Boleng

Davies

A survey of mobility models for ad hoc network research. Wireless Commun Mobile Comput 2002; 2: 483–502.

Meghanathan

Graph theory algorithms for mobile ad hoc networks. Informatica 2012; 36: 185-200.

Clarke

Wing

JM.

Formal methods: state of the art and future directions. ACM Comput Surv 1996; 28: 626–643.

Jensen

Coloured Petri nets: basic concepts, analysis methods and practical use. Vol. 1. Berlin, Germany: Springer-Verlag, 2013.

10.

Kristensen

Soren Christensen

Jensen

The practitioner’s guide to coloured Petri nets. Int J Software Tools Technol Transfer 1998; 2: 98–132.

11.

Reisig

Rozenberg

. Lectures on Petri nets I: basic models: advances in Petri nets. Vol. 1491. Berlin, Germany: Springer-Verlag, 1998.

12.

Ullman

JD.

Elements of ML programming. Upper Saddle River, NJ: Prentice Hall, 1998.

13.

CPN Tools, www.daimi.au.dk/CPNtools (2000, accessed 7 June 2015).

14.

Kristensen

Jørgensen

Jensen

. Application of coloured Petri nets in system development. In: Lectures on concurrency and Petri nets. Berlin: Springer, 2004, pp.626–685.

15.

Xiong

Murata

Tsai

. Modeling and simulation of routing protocol for mobile ad hoc networks using colored petri nets. In: Proceedings of the conference on application and theory of Petri nets: formal methods in software engineering and defence systems, vol. 12, pp.145–153. Darlinghurst, Australia: Australian Computer Society, Inc., 2002.

16.

Khan

Ahmad

Baig

. Formal model of random walk mobility model for WMN using coloured Petri nets. In: 11th international Bhurban conference on applied sciences and technology (IBCAST), 2014, pp.436–444. IEEE.

17.

Agrahari

Chinara

. Simulation of random waypoint mobility model using coloured Petri nets. In: Proceedings of the 2nd International Conference on Computer Science, Engineering and Applications (CCSEA ’12), 2012, pp.65–75.

18.

Resta

Santi

. An analysis of the node spatial distribution of the random waypoint mobility model for ad hoc networks. In: Proceedings of the second ACM international workshop on principles of mobile computing, 2002, pp.44–50. ACM.

19.

Khan

Ahmad

Khan

SA.

Formal and executable specification of random waypoint mobility model using timed coloured Petri nets for WMN. In: Abstract and applied analysis. Hindawi Publishing Corporation, 2014.

20.

Khan

Ahmad

Khan

SA.

Coloured Petri Net modeling and analysis for community based wireless mesh networks. In IEEE international conference on systems, man and cybernetics (SMC), 2014, pp.139–144. IEEE.

21.

Khan

Ahmad

Khan

SA.

SHER: a colored Petri net based random mobility model for wireless communications. PloS One 2015; 10: e0133634.