Research On Formal Verification Method For WSN Routing Protocol Based On ? Calculus

WSN(wireless sensor network) is integrated of computer technology, communication technology and semiconductor technology. It can collect information of target object real time and send it to user, which has important influence on broadening human knowledge and changing the way of human cognition. Comparing with other traditional network, WSN has its own characteristics, such as a large of number of nodes in network, task oriented, poor security, energy and other limited, which makes the design of WSN facing a great challenge.One of the key issues is the design of communication protocol for WSN. Using formal method not only can contribute to verifying the behavior and testing the performance of protocol exactly, but also improving the efficiency of protocol on designing, implementation,verification and testing in the design of communication protocol for WSN.We present an extended ?-calculus, which can model and reason about Wireless Sensor Networks and their routing protocols. The calculus captures the characteristics of WSN,including the limit transmission range and broadcast communication. We also define structural congruence to describe the equivalence relationship between the different nodes of expressions, including jurisdiction domain law, commutative law, and floating law.Transitional rules are also defined in terms of labeled transition systems, which can describe the behavior of communication between nodes. We also define the strong bisimulation, strong bisimulation up to structural congruence and weak bisimulation and use them to verify some properties in WSN. Finally, we illustrate our calculus by developing and analyzing formal models of SPIN routing protocol and a leader election protocol for WSN.