Verification And Analysis Of Self-organization Protocols Of Sensor Networks Based On Model Checking

Wireless sensor networks are self-organizing networks consisting of sensor nodes deployed inthe monitoring area, the correctness and reliability of network protocols are the basis ofself-organizing high-efficiency operations of these networks. During the verification tools ofself-organization protocols in wireless sensor network, model checking is an automated formalverification technique, it can search all behaviors of the system more completely, and find errorsthat can are difficult to uncover. To some extent, model checking can make up for the lackage of testexperiments and simulations.The thesis builds a timed automata model for self-organization protocols of wireless sensornetwork, it sees self-organization as a process of cooperative communication between the sink nodeand sensor nodes, the process is described with timed automata semantics, and timed automata isextended to seven tuples with a probability weighting function which is defined to describe thenon-deterministic of sensor network. On the basis of the timed automata model, the thesis verifiesand analyses the competition-based MAC protocol CSMA/CA, adds energy consumption modeland probability verification method in the timed automata, and creates a different energy models forusing energy harvesting technology to provide energy for sensor nodes, and analyses theperformances of the protocol. The thesis also designs a QoS-based routing protocol GRAC, sets upa timed automata model to verify and analysis of the protocol which uses Dijkstra algorithm toselect the least-cost path as the data transmission path and uses the acknowledgment andretransmission mechanisms to ensure reliability of data transmission.This work in the thesis shows that model checking based verification and analysis can helpimprove the accuracy and reliability of self-organization protocols in sensor networks.