Modeling And Analyzing Of Wireless Sensor Network Protocol Based On Statistical Model Checking

Wireless Sensor Network (WSN) get a great deal of attention along with the developing of wireless sensor technology. WSN have a broadly application scenario. For some dangerous, not easy to reach or difficult to survive situations, the wireless sensors can be used to monitor and control objects. In order to achieve the purpose of monitoring and controlling objects, WSN protocols must ensure functional correctness. At the same time wireless sensors are often resource-constrained, WSN protocols should also consider performance issues.Testing and simulation, theorem provers and model checking technology can be used to ensure the functional correctness of systems.Testing and simulation can not conduct a comprehensive inspection of the system. Theorem provers require expertise handle them. Model checking is an automated, systemative and comprehensive technique that can be used to check the validity of system.In order to analyze the performance of system, we use Statistical Model Checking (SMC) technology. The traditional Model Checking can not cope with the state space explosion problem. SMC uses statistics and simulation method to avoid searching all state space of the system model, and thus refrain from state space explosion problem. So SMC provide a new method to analyze the performance.As a kind of WSN network layer protocol, Minimum Cost Forward (MCF) protocol can form the least cost forwarding path based on cost field. In this process, each sensor node does not require the storage of routing tables. Data can transfer according to the shortest path. It is suitable for WSN.In this paper we focus on the modeling and analyzing of MCF protocol. First, we rebuild Timed Automat (TA) model of MCF protocol, describe the safety and liveness with Timed Computation Tree Logic (TCTL), and analyze the model with the model checker UPPAAL. Then based on the TA model, we model MCF protocol with Priced Timed Automata (PTA) for link error and node failure situations, and analyze the quantitative property using SMC. In addition, the power consumption of the protocol in the case of lossless communication is also analyzed using SMC. Based on the analysis of the experimental results, we find that MCF can perform the routing function of WSN. But the consumption of energy of WSN are not balanced. And when faced with lossy communication, MCF protocol can not fully route data of WSN.