Performance Analyzing Of WSN Time Synchronization Protocol Based On Timed Automata

The Wireless Sensor Network(WSN)'s research originated in the military field.With the need of human development,now it plays an important role in military,medical care,smart home,environmental monitoring,industrial production and business.As far as wireless sensor networks are concerned,time synchronization mechanisms are required in most cases.The time synchronization protocol can provide a common time stamp for the local time of the network node,providing the preconditions for sensing,communication,and energy management functions among the sensor nodes.Due to the protocol is often complicated in the process of development,a bit of error may cause the whole system failure or data transmission error.The analysis of the security,reliability and environmental applicability of the protocol has always been the main content of protocol verification.Model checking is an effective formal method that is suitable for protocol performance verification.This paper adopts the model tool Uppaal which is based on timed automata to construct two typical WSN time synchronization protocols(TPSN and FTSP).This article cites a modeling method for analyzing an wireless sensor protocol network.In the analysis process,the protocol is divided into major parts.The modeling starts from the bottom,and extends according to the specific protocol process.Finally,the complete timed automata model is composed by these parts.From the principle analysis of TPSN and FTSP,it shows that the TPSN process is mainly divided into two phases,a layering phase and a synchronization phase.When the second protocol FTSP is executed,it can be determined that it is also composed of two major local models-sender process and receive process.These local parts of the protocols are the basis for the implementation of modeling with special cases.From above,this analysis method that can be applied to analyze other WSN protocols is determined.In terms of verifying the modeling results,this paper examined the correctness,safety,and liveness of the two protocols.Among them,TPSN has performed correctly in all three aspects;FTSP does not.Based on this result can analyze the cause of the problem.In addition,this paper also extends the price timed automata of the protocol.for a certain number of sensor nodes in a certain period of time,the synchronization data of the two protocol nodes in different environments are recorded.The experimental results can explain the different characteristics of the two time synchronization protocols and their respective applicable environments.At the same time,the evidence of their safety and reliability is also given.