Modeling and Validation of Routing Protocol using Timed Colored Petrinet

Abstract

Now a days, itlis highly importantlto design such a system which is error free and are able to fulfill the users requirement in terms of performance,lefficiency, correctness,lease of use and so forth. Suchlsystems might belapplied in variouslapplications such as communication. Suppose if these system are designed and implemented incorrectly due to some reason. So, it is very important to design such a systems where design errors can be recovered and corrected early. Therefore, Coloredlpetri net is one suchlformal method in whichlmodels depictinglthe exact functionalitylof the system is beinglbuilt, simulated land analyzed. Communicationl protocols, particularly adlhoc routing protocols are additionally one oflthe system which has beenldisplayed and examined to demonstrate the accessibility of specific properties and to find the existinglerrors. Thus, this thesis focuses on modeling an improved version of DSR protocol using Timed Colored Petri nets. DynamiclSource Routing Protocol(DSR) is a routing protocol, where nodes changes their position continuously in the network. In this way it is especially important for each node in the system to monitor changes so that a productive packet transmission should be possible. In this, Timed CPN which is an extension of basic Petri net, which is used to model and validate the working oflDSR protocol in the concurrent environment. Petri nets have been effectively demonstrated the correctness of various communication protocols. DSR protocol is modeled in which an efficient packet transmission is done in the network with the node movement and frequent topology changes. The Timed CPN model aimed to detect and maintain the routes in the dynamic environment and validate the key properties of DSR protocol.