Modeling And Analyzing Wireless Sensor Network Protocols With Stochastic Timed Automata And Statistical Model Checking

Recently, sensor technology has seen significant achievement. Meanwhile, Wireless Sen-sor Network (WSN) technique has attracted lots of attention because of its open and dynamic behaviors, and has become a very important component of the Internet-based computing. The behavior of WSN system is very complex and may encounter lots of stochastic uncertainties and disturbances like message loss and node dynamics. Furthermore, WSN system is diffi-cult to change and maintain once it is deployed. Thus, it is critical to ensure the quality of the low level protocols of WSN system in design phase. Designers should ensure the logical correctness of a protocol, as well as evaluate the performance of the protocol under certain target environments.Compared with simulation and testing, formal analysis gives deterministic verification results against given properties of the system. Therefore, to verify WSN protocols with for-mal method is an important research direction. By now, researchers have used model check-ing technique to check the correctness of protocols. However, there are certain problems in the existing work, such as there is no union method in modeling, the modeling process is unform, and it can only check networks with limited nodes etc. According to corresponding problem, we propose a framework to analyze and evaluate WSN protocols based on stochas-tic timed automata and statistical model checking. Our work mainly focus on the following two aspects:· For modeling, divide a protocol into different phases according to its work flow, then model each phase separately, and finally get the whole classical timed automata in the bottom-up way. Then, to model the uncertainties such as message loss and node dynam-ics, which are common in realistic circumstances, the timed automata can be extended by weighted transitions, resulting in the stochastic timed automata.· For analysis and verification, the correctness of the protocol can be checked by classical model checking on the timed automata, while the performance of the protocol under realistic environments can be evaluated by statistical model checking on the stochastic model.To illustrate the details and feasibility of the modeling and verification method, two WS- N time synchronization protocols, Timing-sync Protocol for Sensor Networks (TPSN) and the Flooding Time Synchronization Protocol (FTSP) are studied completely throughout the paper. Timed automata and stochastic timed automata are built for these two protocols. Based on that, we use model checking and statistical model checking technologies to verify and an-alyze these protocols. By our method, we find FTSP has drawbacks in its design. Under specific conditions, the leader election algorism of FTSP can not work correctly. Meanwhile, although the design logic of TPSN is correct, its performance is sensitive with the environ-ment and can’t work well in harsh environments. These results illustrate the effectiveness of the proposed method in our paper.On the other hand, protocol designers may come across difficulties when modeling and verifying a protocol directly, it needs long time study and training. This is the reason why the model checking can not be used widely in relevant field by now. To solve these problems, we design a WSN Protocol Description Language (WPDL) based on protocol flow diagrams, which designers are familiar with. With the WPDL, the designers can describe protocol conveniently. Based on WPDL, an Assistant Modeling Tool (AMT) is developed to build timed automata model of a protocol automatically. Compared with the original modeling process, this process is simplified, and can reduce most of the work.