Opportunistic Routing Protocol For Wireless Sensor Networks Based On Probabilistic Model Checking

Wireless sensor network (WSN) is comprised by those sensor nodes which has the abilites ofsensing, processing and wireless communication and capable of self-organization. Opportunisticrouting is a data forwarding protocol which can be adopted to wireless sensor network, nodes woulddetermine its priority by the specific metric with the destination node, and the highest priority nodein a group will be forwarding packets to another group of nodes, until the packet arrives ondestination node.This thesis verifies and analysises typical opportunistic routing of the low duty-cycle WSN andmobile WSN based on probabilistic model checking technology separately, and improves theseprotocols. Detail studying contains three aspects as follows:(1) Classical opportunistic routing of the low duty-cycle WSN is modeled, analyzed andverified by probabilistic model checking method. The verifying result shows the problem of highempty nodes rate. Aiming at this problem, the opportunistic routing with backtracking (LDCOP)has been designed to improve the problem of empty nodes. Its main idea is that if a next hopminimizing the remaining distance is not found during the maximum waiting time; the packet is notdiscarded, and the protocol allows the packet to initially move further away from the sink until apath to the destination is found. Then the tool model checking PRISM is used to check LDCOP andfind it has a better performance in packet forwarding rate and reducing empty nodes.(2) Opportunistic routing of mobile WSN is modeled, analyzed and verified by probabilisticmodel checking method. The verified result shows the problem of short survival time. Aiming atthis problem, Opportunistic routing based on energy aware and load balancing (PAGeRaF) isdesigned to solve the problem. This protocol improves the priority of candidate forwarding set. Itjoins the energy aware and load balancing. Then the tool PRISM is used to check PAGeRaF andfound it has prolonged the survival time of the network.(3) The PAGeRaF is applied to VANET; the road density discovery and neighbor discoverymechanism are analyzed, and the PAGeRaF based VANET is simulated and analyzed using NS2inthe actual application scenarios, which shows that PAGeRaF can effectively reduce the number ofnetwork messages to avoid channel congestion compared with the traditional AODV routing.