Hierarchical Coloured Petri Net based random direction mobility model for wireless communications.
Wireless communications has become omnipresent in the world and allow users to move anyway and to communicate with other nodes. Wireless mesh networks (WMNs)  have gained incredible attention of research community due to its numerous benefits viz., extremely adaptable, expandable, wide coverage, high speed mobility, high quality video surveillance and low cost both for fixed and mobile users. At one point it is considered that mobile ah-hoc network (MANET)  is branch of WMNs, so mobility management strategies can be applied to WMNs.
Mobility of a user is prominent benefit of wireless over fixed communication while mobility model is its integral component. In the performance evaluation of developed network model, using a realistic mobility model is essential for obtaining credible results. Thus, the most suitable mobility model is necessary when evaluating the network performance. Further, it is necessary that underlying chosen mobility model should emulate closely the real life scenarios in the success of research analysis  otherwise misleading results may be drawn from these simulations. Trace based mobility modeling is credible approach to extract realistic trajectories, however as WMNs are not yet implemented on large scale, so obtaining real traces is a crucial task. Therefore, several mobility models have been presented with diverse characteristics, an exhaustive survey is published in . Mobility models have been classified in to four categories, random base, with temporal dependency, with spatial dependency and with geographic restrictions as shown in Fig. 1.
[FIGURE 1 OMITTED]
Traditionally, the simulation is considered the most effective way to design and evaluation of wireless models due to its numerous benefits viz., forecasting under uncertainty, low data requirements and low cost, but literature reflects that occasionally it suffers from some issues, like fidelity and validity of the simulation results and acquisition of valid source information. Formal Methods  have tremendous potential for precision of requirements and to prove or disprove correctness of proposed model because these methods are based on mathematics and logic. This approach provides insights into the system requirements and basis for elegant critical systems, further they are provable. This reduces requirements omissions and reveling subtle errors. They are usually motivated due to power of localizing proposed models to small parts where you can check existence of dead-locks or live-locks etc. Traditionally, Internet Engineering Task Force (IETF) has adopted specification process through informal English pros, which is ambiguous and mostly created hit and trail based software development culture. The research community is converged that formal methods are not only grossly adequate for specification, analysis and validation of systems but are also poised to play a central role in development of communication protocols, secure software systems, programming languages, engineering systems etc. Formal methods adjunct tools examine the complete state space of system to detect critical issues and to catch subtle design errors before design coding phase.
Coloured Petri Nets (CPNs or CP-nets) , are type of Petri Nets  that are used in modeling of systems which contain discrete, concurrent and scattered events and had strong mathematical logic associated with Standard ML (SML)  programming language.
They are useful in modeling both non-deterministic and stochastic processes and allow a systematically exhaustive exploration of the mathematical model to prove, disprove or analyze correctness of various communication systems, operating systems, business process and re-engineering . The CPN comes with graphical interface which makes it an easy to use, understand and user-friendly CPN tools  with extensive documentation and support. In CPN untimed models are mostly used to reveal logical errors while timed nets for concurrent systems. Most importantly, CPNs allow modeling of both timed and untimed executable nets. CPN supports strong mathematical foundation for state space and reachability analysis to verify numerous properties viz., boundedness, home, liveness, fairness, terminating and cyclic. To overcome state explosion problem state space reduction methods are implemented through Linear-time temporal logic (LTL) or Computation tree temporal logic (CTL). The other significant feature is that, the model can be divided into different modules in traditional hierarchical manner.
Random direction mobility model is the modification of random waypoint model , . Mobile hosts (users) move randomly and freely in any direction in such type of mobility models. Further the direction, speed and destination of a mobile host is based on random decisions.
This paper presents first time CPNs based implementation, execution and verification of renowned Random Direction Mobility Model . We constructed 100 x 100 [m.sup.2] terrain, where a mobile host can move randomly according to Random Direction Mobility Model theory. In the given simulation setup, a node selects a random destination in the defined 100 x 100 [m.sup.2] communication region with speed between 0 to its upper limit. The node travels to its randomly chosen destination and stops for a random period of time before selecting next itinerary. This behavior is repeated independently again and again for the length of defined simulation. This has been done by defining the timed transitions in the detailed CPN model. The proposed model provides a foundation and has potential for validation of mobility management strategies and routing protocols in wireless communication.
The remainder of the paper has following structure. Section 2 analyses related work associated with our contribution. Section 3 presents Random Direction Mobility Model theory and CPN based proposed formal model. Further, state space analysis and validated results are outlined in Section 4. Finally in Section 5 we concluded our achievement with future direction.
2. Related Work
The mobility models have myriad uses in wireless communication and play crucial role in performance evaluation of different wireless network scenarios. Underlying mobility model can help answer varied routing protocol related questions. In , an effort was made to present four case studies viz., modeling scenarios in Ad Hoc Networking, modeling requirements in Pervasive Healthcare, state space analysis of an audio/video protocol and implementation of planning tool. The first part presents the mobility specifications and communication scenarios in the ad-hoc networks. Both the micro and macro mobility cases were abstractedly modeled. The model is most appropriate for mobility test cases. The first systematic study to present CPN based formal model of MANET was carried out in  where authors focused on mobility issue and proposed topology approximation (TA) algorithm. The results verified that the proposed mechanism handles mobility without topology information. Khan et al.  proposed formal model of random walk mobility model for WMN, by eliminating border effect and speed decay issues. The CPN model is able to produce numerous diverse mobility trajectories. The CPN based RWP mobility formal model was proposed in , despite their efforts there is need of its further improvements as model in not producing mobility patterns of user. In order to produce more realistic movement patterns, Khan et al proposed RWP mobility model in  without border effect and speed decay problems.
CPN based modeling revealed a lot of advantages, which have been discussed above. The literature reflects that much work has not been done to resolve mobility issues and this can add benefits in the direction of simulation modeling for the wireless networks. A CPN based formal model for community wireless mesh network is presented in , which is not only flexible but also extendable. In this model a mobile node can freely moves and sends data packets to other nodes. SHER ("Show Home and Exclusive Regions") random mobility model is proposed in , where six key issues of random models have been removed viz., sudden stops, memory less movements, border effect, temporal dependency of velocity, pause time dependency and speed decay. The model produces five hotspots based on frequency of visits of mobile hosts. Significant efforts were made in , where authors presented a highly flexible trajectory model based on the primitives (integrals) of Brownian fields (BFs) to track the location of the mobile station (MS), performance analysis and channel modeling. Random closed-loop trajectories and both targeted and non-targeted dynamics of user can be obtained. They studied statistical properties viz., autocorrelation function (ACF), mean, variance and also derived distribution of the angle of motion (AOM) process. Recently an improved Random Direction Mobility Model is proposed in , where authors removed short turn problem of the model.
3. CPN BASED MODELING FOR RANDOM DIRECTION MOBILITY MODEL
3.1 Theory of Random Direction Mobility Model
The synthetic Random Direction model was first time proposed in  and is benchmark due to its simplicity. In this model each mobile node is independent; first every node selects a degree between (0-359) and finds a destination on boundary of terrain in the selected direction. After that mobile host (MH) randomly selects speed to travel. Upon reaching the destination, the MH pauses for a certain period, after stay host again finds new destination and moves towards this with new speed and complete second itinerary. The same process is repeated till the simulation stops.
3.2 Environment Scenario
The Random Direction hierarchical CPN Mobility Model consists of three levels as depicted in Fig. 2. The model has dynamic capabilities, so mobile host [N1 .. [N.sub.n]] can randomly be spread in 100 x 100 [m.sup.2] communication area. The scenario illustrated in this paper shows the initial state of model with five MH. Each mobile node has its own itinerary.
[MH.sup.1],0,(10,1),(0,55), [MH.sup.2],5,(59,26),(59,100), [MH.sup.3],8,(39,28),(69,0), [MH.sup.4],1,(33,47),(0,80)
[FIGURE 2 OMITTED]
MH2 arrival time is 5 at location (59, 26) coordinates and its destination is (59,100). Model is as abstract view, however user can enhance nodes. Time clock is considered in Minutes.
[FIGURE 3 OMITTED]
In Fig. 3 above scenario is reflected, arrival location is represented with black dot while destination location is represented with green dot. CPN Model presents an abstract view of the system, however, nodes can be enhanced. Approximate transmission range of 802.11n based MH transmitter is 250 m. The time clock is considered in Minutes.
3.3 Hierarchical pages of CPN Model
Top level view of the hierarchical CPN is depicted in Fig. 4, which represents the most abstract form of the system. The "TOP" node in Fig. 2 has been represented by the corresponding top-level view given in Fig. 4. The rectangle RANDOM DIRM M in Fig. 4 is the substitution transition as indicated by the associated HS-tag.
[FIGURE 4 OMITTED]
The Substitution transition has an associated subpage, which is given in Fig. 5, representing the compound behavior. The ellipses in Fig. 4 are the places for top-level model and represent different objects of the system. Place ND represents the total MH available, the place DESTI shows the number of completed epochs. Place BACK BONE represents current movement patterns of the nodes and serves as the backbone for WMNs.
[FIGURE 5 OMITTED]
The "RDIRMM" node in Fig. 2 has been represented by the corresponding page in the Fig. 5 which presents the process model of random direction mobility patterns. Detail of the transition RANDM DIRM M specifies the main functionality of the RDM model. The place ND in this page, given in Fig. 5, is called the port place which shows the total nodes and it has the same representation as discussed for top level model (see Fig. 4). The transition HOME is a substitution transition (its details are given in Fig. 6) and generates the MH's initial status. Transition NEW ROUTE is also a substitution transition (its detail model is shown in Fig. 7) and generates a new route after completion one epoch. The transition INSTANT MOVE is more important transition and generates the MHs movement patterns. The place BACK BONE is a port place, which is already shown in Fig. 4, and it monitors the movements of all the nodes. Speed token is generated through the transition Speed which has input place Slect Speed.
[FIGURE 6 OMITTED]
The "HOME" node in Fig. 2 has been represented by the corresponding page in Fig. 6 which illustrates the detail model of HOME transition specifying the MH initial status. The transition Time_of_Arrival generates a multi-set, shows MH number and arrival time, e.g. ("MH-1", 5), here MH identity is 1 and arrival time is 5. The place ND (also given in Fig. 5) provides the input this sub-module in the form of the number of mobile hosts. Further, the sub-module of Fig. 6 generates the output in the form of mobile host id with its time in the place MH1. Moreover, transition HOM generates initial coordinates and transition START produces 6-tuple element, i.e. 1'(("MH-1",0),0,(36,8),(36,8),3, START)@0, of a multi-set as an output. The element of multi-set gives that the MH id is 1, step number is zero, its home coordinate and current coordinate is (36, 8), direction is 3 and the node status is START. The "NROUTE" node in Fig. 2 has been represented by the corresponding page in the Fig. 7 which shows the low-level net of the transition NEW ROUTE given in Fig. 5. The main functionality of this module is to generate a route in a new direction after completion of one epoch.
[FIGURE 7 OMITTED]
The transition NEW EOPCH is an important transition having one input arc from the place EOPCH of Fig. 5, which provides input to the sub module in the form of new routes. It also has four input/output double ended arcs and 2-output arcs which generates the new random route.
3.4 Color sets
The colour set NO is assigned to the place ND in Fig. 4 which is a set of integers from 1 to tn and it specifies the range of a MH, i.e. total mobile hosts in the model, where 1 [less than or equal to] n [less than or equal to] tn. It is important to mention that some colour set and variable names have been taken from . The colour set NODE has been assigned to the place MH1while NODE is a Cartesian product of the set ID of string type and the set ART showing arrival time. Colour set STATUS is of free type with three categories, which are a start, traveling and finish. The place HOME in Fig. 7 has a colour set MH which is a product of NODE, STEP, COORD, INT and STATUS (see Table 1). Moreover, colour set MH is a multi-set with six-tuple elements. Colour set BBONE is assigned to the place BACK BONE shown in Fig. 4 and Fig. 5, which is the product of the sets, NODE, INT, STEP, COORD and STATUS (see Table 1). This colour set is a multi-set with 7-tuple elements representing the node id, time, step number, home and current coordinates, the direction of the node and its current status.
3.5 The Traveling Sequence
As simulation starts, the place ND generates all mobile hosts in the system while the place St-Time generates the starting time. When transition Time of Arrival fired, a token with arrival time moves to the place ND AT in Fig. 6. The transition HOM generates starting x-axis and y-axis values for the MH in the place RHOME. Further, the transition START generates a 6-tuple multi-set which has elements in the form, e.g. 1(("MH1",0),0,(76,5),(76,5),1,START)@0, in the place MH1. It illustrates that MH ID is 1, start time = 0, home coordinates are (76, 5), current coordinates are (76, 5), direction is 1, status is START and at system time is 0. Therefore, the sub-module (HOME page in Fig. 6) takes the number of MHs as input and generates the 6-tuple multi-set as output in the place MH1. In addition, the transition Speed in Fig. 5 enables and captures speed from 1..5 from the placeSlct SPEED. As token moves to the place WPEED and the transition INSTANT MOVE enables. This transition has 2-Input and 5-output arcs. By firing this transition, the token again moves back to the place HOME. The repeat process starts until 1st epoch completes. Meanwhile BACK BONE place monitors all the records of MH's which further are used in routing protocol analysis. After completion of the 1st epoch the transition NEW EOPCH enables in the module NROUTE (see Fig. 7) and by occurring this transition, a new route's tuple is added at place HOME. Thereafter, this process is repeated again and remains continue until simulation ends. Fig. 8 illustrates the high-level view after 2500 steps with timestamp 117.
[FIGURE 8 OMITTED]
The top page is presenting 47 completed trajectories by 20 nodes i.e. MH-1 to MH-20, while at BACK BONE place there are 2211 tokens reflecting individual movement patterns. The routes of 3-mobile nodes after 500 Steps and 188 time stamp simulation is depicted in Table 2.
4. SIMULATION ANALYSIS AND DISCUSSION
To simulate and validation of proposed formal model, state space analysis are used where we can verify properties like, boundedness, home, fairness, live-locks and dead-locks etc. The partial state space analysis for 1 node is presented in Table 3, it demonstrates that Occurrence graph (O-graph) has 39815 nodes and 73397 arcs. Further, there exists Strongly Connected graphs (SSG), so the model has infinite occurrence sequences. Mobile host can move in region without any restriction. Upper and lower bounds properties specify top and lower limits of tokens that can reside in a place.
The place ST-Time has both upper and lower bounds with 11 tokens, these tokens represent the arrival time of a MH. It is shown that there are 6458 dead markings (see Table 3). The sentiment expressed for this situation that these states are deadlocks in the state space generated through the model. Such type of dead states can be interpreted as final or terminal states of the system. Moreover, it is interpreted that when the simulation terminates in the model, it ends with accurate and as per required specifications.
HOME to DESTINATION paths for single mobile nodes have been reflected in Fig. 9. The random direction mobility model represents unlimited navigation within the system. MH starts traveling from the coordinates (26, 69).
There are 79 completed trips and every trip ends up on boundary of the terrain.
[FIGURE 9 OMITTED]
The proposed model represents unlimited navigation within the system. In order to evaluate the performance of the model and to verify deadlock freedom. We gradually increased number of mobile nodes in the model and observed statistical results. Fig. 10 demonstrates that 1 node completed 12 trips in 500 simulation steps while 49 trips in 2500 steps. The proposed model is expandable and to validate this we increased number of nodes to 10,20,30,40 and 50 against number of simulation steps i.e. 500, 1000, 1500, 200 and 2500 respectively. The numbers of completed trips are dependent on speed and angle of destination, therefor the trips are variable against the different number of nodes and steps.
The outcome is reflected in Table 4, it is evident that the model is not only deadlock free but also expandable. The performance of model remains almost same against the number of simulation steps, e.g. single MH have completed 49 trips in 2500 steps, 10 nodes completed 52 trips in 2500 steps while 50 MH completed 50 trips in 2500 steps.
[FIGURE 10 OMITTED]
Mobility modeling is an emerging branch and fundamental component of wireless networks. At the time of writing, a CPN based formal model of well-known Random Direction Mobility model has been proposed in this paper for the first time. Most of the existing research on mobility models is based on conventional simulation tools, e.g. NS-2, OPNET, OMNet and QualNet simulators. We envisage that our work, based on formal approaches, will open a new paradigm of research. The proposed model is flexible because a user can specify total number of mobile nodes for movement in communication area. The model then randomly selects arrival time, home coordinates, speed and destination direction for first epoch. After reaching boundary line mobile node pauses for some time and then selects new destination. The outputs of model are trace like, these can further be utilized in evaluation of routing protocols and mobility management strategies in wireless communication. Further, a user can generate different mobility patterns under various topologies. To validate the performance extensive simulations were conducted under different scenarios. For its future improvements, there are many directions like, inclusion of obstacles, static structures, hot spots and history based movements.
 I. F.Akyildiz, X.Wang, W.Wang, "Wireless mesh networks: a survey," Tech. rep., Georgia Institute of Technology, Computer Networks, Volume 47, Issue 4, pp 445-487, March 2005. Article (CrossRef Link).
 Y. Chaba and N. K. Medishetti, "Routing protocols in Mobile Ah hoc Network-A Simulation Study Final," JCS Vol 1, No. 1, August 2005.
 P. Stephane, T. Joanna, V. Veronique, "A Composite Mobility Model for Ad Hoc Networks in Disaster Areas," REV Journal on Electronics and Communications, Vol. 1 No. 1,pp 62-68, March 2011.
 N. Aschenbruck, A. Munjal and T. Camp, "Trace-based mobility modeling for multi-hop wireless networks," Computer Communications, vol. 34, pp. 704-714, 2011. Article (CrossRef Link).
 E. M. Clarke and J.M Wing, "Formal Methods: State of the Art and Future Directions," ACM Computing Surveys, 28(4), pp 626-643, December 1996.
 K. Jensen, "Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use," Vol 1-3. Monographs in Theoretical Computer Science. Springer-Verlag, 1997. Article (CrossRef Link).
 L.M. Kristensen, S. Christensen, and K. Jensen, "The Practitioner's Guide to Coloured Petri Nets," International Journal on Software Tools for Technology Transfer, 2(2), Springer-Verlag, pp 98-132, 1998.
 J. Billington, M. Diaz, and G. Rozenberg, editors, "Application of Petri Nets to Communication Networks," Advances in Petri Nets, Volume 1605, Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1999. Article (CrossRef Link).
 W. Reisig and G. Rozenberg, editors, "Lectures on Petri Nets: Advances in Petri Nets," Volume I: Basic Models, Volume 1491, Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1998. Article (CrossRef Link).
 J. D. Ullman. "Elements of ML Programming". Prentice-Hall, 1998.
 Mitsche, D., Resta, G., & Santi, P., "The random waypoint mobility model with uniform node spatial distribution," Wireless Networks, Vol. 20, 1053-1066, 2014. Article (CrossRef Link).
 Camp, T., Boleng, J., & Davies, V., "A survey of mobility models for ad hoc network research," Wireless communications and mobile computing, 2(5), 483-502, 2002. Article (CrossRef Link).
 CPN Tools: www.daimi.au.dk/CPNtools.
 E. M. Royer, P. M. Melliar-Smith, and L. E. Moser, "An analysis of the optimum node density for ad hoc mobile networks," in Proc. of the IEEE International Conference on Communications, June 2001. Article (CrossRef Link).
 Lars Michael Kristensen, Jens Bsk Jorgensen, Kurt Jensen, "Application of Coloured Petri Nets in System Development," Lectures 626-685, 2003.
 Xiong C., Murata T., Tsai j., "Modeling and Simulation of Routing Protocols for Mobile Ad Hoc Networks Using Colored Petri Nets," in Proc. of Conferences in Research and Practice in Information Technology, Vol 12, 2002.
 N.A.Khan, F.Ahmad, and W.A.Baig, "Formal Model of Random Walk Mobility Model for WMN using Coloured Petri Nets," in Proc. of 11th International Bhurban Conference on Applied Sciences & Technology (IBCAST), pp. 436-444, 2014. Article (CrossRef Link).
 S. Agrahari and S.Chinara, "Simulation of Random Waypoint Mobility Model Using Colored Petri Nets," in Proc. of on the Second International Conference on Computer Science, Engineering and Applications (CCSEA-2012), pages 65-75, 2012.
 NA Khan, F. Ahmad, and SA Khan, "Formal and Executable Specification of Random Waypoint Mobility Model Using Timed Coloured Petri Nets for WMN," Abstract and Applied Analysis, vol. 2014, Article ID 798927, 9 pages, 2014.
 Khan, NA, Ahmad, F., & Khan, SA., "Coloured Petri Net Modeling and Analysis for Community based Wireless Mesh Networks," in Proc. of the IEEE International Conference on Systems, Man and Cybernetics (SMC), 2014, pp 139-144, San Diego, CA, USA, 5-8 Oct. 2014. Article (CrossRef Link).
 Khan NA, Ahmad F, Khan SA., "SHER: A Colored Petri Net Based Random Mobility Model for Wireless Communications," PLoS ONE 10(8):e0133634.doi: 10.1371/journal.pone.0133634, August, 2015. Article (CrossRef Link).
 A. Borhani and M. Patzold, "A highly flexible trajectory model based on the primitives of Brownian fields--part I: Fundamental principles and implementation aspects," IEEE Trans. Wireless Commun., vol. 14, no. 2, pp. 770-780, Feb. 2015. Article (CrossRef Link).
 A. Borhani and M. Patzold, "A highly flexible trajectory model based on the primitives of Brownian fields--part II: Analysis of the statistical properties," IEEE Trans. Wireless Commun., vol. 15, no. 1, pp. 247-257, Jan. 2016. Article (CrossRef Link).
 Khan NA and Ahmad F., "Modeling and simulation of an improved random direction mobility model for wireless networks using colored Petri nets," Simulation: Transactions of the Society for Modeling and Simulation International 2016, Vol. 92(4) pp 323-336, April 2016. Article (CrossRef Link).
Naeem Akhtar Khan (1), Farooq Ahmad * (2), Syed Asad Hussain (2), Mudasser Naseer (2)
(1) Faculty of Information Technology, University of Central Punjab Lahore, Pakistan [firstname.lastname@example.org]
(2) Department of Computer Science, COMSATS Institute of Information Technology, Lahore, Pakistan [E-mail: email@example.com, firstname.lastname@example.org, email@example.com]
* Corresponding author: Farooq Ahmad
Received January 8, 2016; revised April 25, 2016; accepted June 24, 2016; published August 31, 2016
Naeem Akhtar Khan received the M.S. degree in Computer Science from University of Agriculture, Faisalabad, Pakistan in 2008. He is currently PhD (Computer Science) scholar in Faculty of Information Technology, University of Central, Punjab, Lahore, Pakistan. His research interests are in the area of 4th Generation Wireless Networks, Mobility Management and Formal Methods (Coloured Petri Nets).
Farooq Ahmad is currently an Associate Professor in the Department of Computer Science, COMSATS Institute of Information Technology, Lahore, Pakistan. He received his PhD degree in Computer Science from Harbin Institute of Technology, China. He has numerous publications in reputed international journals. He has been the vice-chair of IEEE Computer Society Lahore Section for 2011-12. He has been the conference co-chair as well as an invited speaker in several national and international conferences. His research interests are formal modeling, verification and simulation and Petri net theory and applications.
Syed Asad Hussain is working as a professor and dean faculty of information science and technology at COMSATS Institute of Information Technology Pakistan. He is currently leading communications networks research group at the department of computer science COMSATS Institute of Information Technology Lahore Pakistan He obtained his Master's from University of Wales, Cardiff, UK and PhD from the Queen's University Belfast, UK. He was funded for his PhD by Nortel Networks UK. He was awarded prestigious Endeavour research fellowship by Australian Government for his post doctorate at the University of Sydney, Australia in 2010, where he conducted research on VANETs. He has taught at Queen's University Belfast UK, Lahore University of Management Sciences (LUMS) and University of the Punjab. Currently he is supervising PhD students at CIIT and split-site PhD students at Lancaster University, UK. His area of research and teaching is communication networks. He has authored and co-authored more than 45 journal and conference papers and has written a book titled Active and Programmable Networks for Adaptive Architectures and Services. This book has been published by Taylor and Francis USA. He has been a member of IEEE. He regularly reviews international journals and conferences papers.
Mudasser Naseer is working as an Assistant Professor in the Department of Computer Science of COMSATS Institute of Information Technology, Lahore, Pakistan. He did his PhD in 2010, in Computer Science from Beihang University (Beijing University of Aeronautics and Astronautics), China. His research interests are Non Linear Dimensionality Reduction, Pattern Recognition, Machine Learning and Computational Statistics.
Table 1. Definition of color sets Color Set Definition colset NO = int with 1..tn Specifies the range of MH timed; colset ID = string; Node ID , String type colset STIME = int with Defines System Time 0..stime; colset NODE = product ID*ART Product type with node ID and timed; arrival time. colset COORD = product COR*COR; Product Color Set for Coordinates colset STATUS = with START | Specifies current state of MH TRAVELING | FINISH; with 3-types. colset MH = product Timed MH color set 6-tuple, NODE*STEP*COORD*COORD*I consists of Node ID, Step No., NT*STATUS timed; Home, Current, Direction and Current status. colset BBONE = product Very Important Color set, NODE*INT*STEP*COORD*COO Cartesian product type 7-tuple, RD*INT*STATUS timed; Node ID, Time, Step No. Home, Current, Direction and current Status. Dynamics (User defined parameters) val tn = 10; The symbolic constant tn specifies total number of MH in the system, where 1 [less than or equal to] n [less than or equal to] tn val xlimit = 100; Terrain ranges x-axis and y-axis val ylimit = 100; 1 to xlimit val stime = 10; colset STIME = The symbolic constant stime int with 0..stime; specifies total Arrival time of MH in the system, where 1 [less than or equal to] n [less than or equal to] stime Home Coordinates (hx) & (hy) Home Coordinates can be enhanced (discrete(0,99) as per xlimit & ylimit Speed limit (1..n) Speed of MH can be fixed for single epoch as (1..n) The Functions fun SysTime() = Generate System Time in Integer IntInf.toInt(time()); form. fun AT() = discrete(1,10); Specifies the Arrival Time of MH fun ran () = discrete (0,100); Random Function generates number between 0 .. 100. fun CNTR Function increases each step of (cx,cy,xlimit,ylimit,steps)= if movement. (cx=0) orelse (cx = xlimit) orelse (cy = 0) orelse (cy = ylimit) then steps else steps+1; fun CSTATUS Specifies current status of MH, (cx,cy,hx,hy,xlimit,ylimit) = if either START, TRAVELING or (cx=0) orelse (cx = xlimit) FINISH. orelse (cy = 0) orelse (cy = ylimit) then FINISH else if (cx,cy) = (hx,hy) then START else TRAVELING ; fun MOVE Takes 6 inputs and generate next (cx,cy,xlimit,ylimit,d,sp) step to move. Table 2. Movements after 500 steps NODE 1, completed 5 epoch in 184 m 1'(("MH-1",0),1,1,(97,89),(100,86),FINISH)@2+++ 1'(("MH-1",0),25,14,(100,86),(86,100),FINISH)@26+++ 1'(("MH-1",0),49,27,(86,100),(100,86),FINISH)@50+++ 1'(("MH-1",0),73,40,(100,86),(86,100),FINISH)@74+++ 1'(("MH-1",0),183,139,(86,100),(86,0),FINISH)@184+++ NODE 2, completed 3 epoch in 188 m 1'(("MH-2",9),103,94,(54,94),(54,0),FINISH)@104+++ 1'(("MH-2",9),123,103,(54,0),(100,46),FINISH)@124+++ 1'(("MH-",9), 187,156,(100,46),(46,100),FINISH)@188+++ NODE 3, completed 3 epoch in 148 m 1'(("MH-3",6),27,21,(74,79),(74,100),FINISH)@28+++ 1'(("MH-3",6),111,94,(74,100),(0,26),FINISH)@112+++ 1'(("MH-3",6),147,119,(0,26),(26,0),FINISH)@148 Table 3. Statistics for O-Graph State Space Nodes: 39815 Arcs: 73397 Secs: 300 Status: Partial Scc Graph Nodes: 39815 Arcs: 73397 Secs: 5 Boundedness Properties Best Integer Bounds Upper Lower HOME'CNTR 1 1 0 HOME'DIR 1 8 8 HOME'MH 1 1 0 HOME'ND AT 1 1 0 HOME'RHOME 1 1 0 HOME'St 1 11 11 NROUTE'DIRECTION2 1 3 3 NROUTE'DIRECTION4 1 3 3 NROUTE'DIRECTION5 1 3 3 NROUTE'NEW ROUTE 1 1 0 Dead Markings 6458 [59,50,40,39815,39814, ...] Live Transition Instances None Fairness Properties No infinite occurrence sequences. Table 4. Throughput of the Model- number of Steps VS number of Trips Nodes 500 1000 1500 2000 2500 Steps 1 MH 12 20 30 41 49 Trips 10 MH 11 24 35 44 52 Trips 20 MH 10 21 31 37 47 Trips 30 MH 10 20 28 44 51 Trips 40 MH 6 15 27 34 45 Trips 50 MH 3 11 27 37 50 Trips
|Printer friendly Cite/link Email Feedback|
|Author:||Khan, Naeem Akhtar; Ahmad, Farooq; Hussain, Syed Asad; Naseer, Mudasser|
|Publication:||KSII Transactions on Internet and Information Systems|
|Date:||Aug 1, 2016|
|Previous Article:||Data sorting-based adaptive spatial compression in wireless sensor networks.|
|Next Article:||Novel preamble design for channel estimation in FBMC/OQAM systems.|