Static Analysis Of Routing Protocol Implementations For Wireless Sensor Networks

Wireless sensor networks has been widely used in environmental monitoring, military, aviation and other fields because of its low price, ease of deployment, scalability, etc. Meanwhile, much more attention has been paid to the correctness of WSNs routing protocol and its implementations.Over the past years, researchers have mainly focused on design, modeling and verification of WSNs routing protocols and has made a lot of progress. However, the analysis of WSNs routing protocols is only a little. After the design, implementations of the routing protocol, it needs to be embedded into sensor nodes. Even if the protocol design is no problem, because of the unreliability of the protocol implementation code, we cannot guarantee that communications between sensor nodes in accordance with protocol specifications, so it is very necessary to analyze WSNs routing protocol implementations. WSNs nodes are generally based on specific sensor nodes and protocol implementations are usually embedded applications. While embedded applications are difficult to be dynamically analyzed, and therefore we propose using static analysis approaches to study WSNs routing protocol. First, we introduce the characteristics of WSNs routing protocol and its implementations; and then, we propose a static analysis framework for WSNs routing protocol implementations, further we analyzes the practical application of WM2 RP enterprise routing protocol using our proposed approach. Specifically, the main contributions of this paper are:(1) Analyze and summarize the characteristics of WSNs routing protocol and its implementation code, research and compare the existing program static analysis tools.(2) Propose a static analysis framework for WSNs routing protocol implementations, which can analyze both common protocol code memory error, but also checking protocol that meets the protocol specification, and can analyze dimensional problem of protocol implementation codes. At the same time, we develop the dimensional analysis tools based on KLEE and implements some functions.(3) According to a practical WM2 RP protocol document and the protocol implementation codes, we abstract its protocol specification, then, we analyze its implementations codes using our proposed static analysis of WSNs routing protocol implementations. The analysis results of WM2 RP routing protocol implementations have a good reference value for the protocol developers.