The Modeling And Analyzing Of Data Gathering Protocol For Wireless Sensor Networks

Wireless sensor networks (WSN) has been widely applied to provide aconvenient and ensurence of security. There are lots of WSN, for example, firealarming, environment monitoring, gas meter reading and other areas. WSN has agreat impact on people’s lives. Data collection is the main function of wireless sensornetworks, with data collection protocols used widely in different areas. So datacollection protocol analysis technology gets more and more attention.In this paper, the demand for real-time data collection protocols, the researchmethod of modeling and analyzing WSN data collection protocol is proposed, whichis based on the real-time model checker UPPAAL.UPPAAL is a model checker, based on timed automata theory and jointlydeveloped by Aalborg University and Uppsala University. Since the input modelUPPAAL is very complex, including the migration time constraints, the stateresidence time constraints and interactive communication among time automata, etc.So it is difficult for user to directly and accurately use the input model of UPPAAL.Aiming at this problem, a two-stage modeling approach was propoesd:first,creatingthetime automata model of the communication behavior of selected data collectionprotocol, further translating it to the input model of UPPAAL.To illustrate theeffectiveness of this method, we choose an actual wirelessmeter data collectionprotocolRMT as an example,using UPPAAL toanalyze its nature and developingsupport toolfor automated analysis. The main contributions of this paper are:(1) Propose a modeling and analyzing method for data collection protocol ofWSN: creating automaton model firstly, and then refine the model to the input modelof UPPAAL for validation of protocol.(2) Use the proposed method for modeling and analyzing practical wireless meterreading data collection protocol RMT.(3) Develop a tool to support automatic verification and optimization of RMTprotocol.