Colored Petri Net-based Spin Protocol Verification

As a new technology, wireless sensor networks has become the research focus of the current international,it is considered to be one of the technologies that have a tremendous impact on people's lives in the 21st century. The study of routing protocols in wireless sensor networks is an important research field. To analysis and verify exist protocols, make sure that these exist protocols is available for wireless sensor networks is a very important direction. SPIN is the first data-based routing protocol of wireless sensor networks. It uses the mechanism of negotiation and resource-adaptation to overcome the problems of tradition protocols, saves energy and extends the life of the network. SPIN has two protocols, SPIN-1 and SPIN-2.At present, the research of SPIN is mainly simulated in the NS platform, and analyse the performance of the procotol. This paper is from another perspective of using formal methods to verify the protocol. First, the paper were using colored Petri Net to analyse SPIN-1 and SPIN-2, and gives their CPN models. Afterwards, we simulated these two models by automated analysis tools CPN Tools, and gained occurrence graph and correlated analysis report. According to these, the paper verified that the two protocol has characteristics of liveness, reachability and boundedness.SPIN was design for ideal lossless network, it didn't considered the loss of packets in the actual network. To this issue, the paper brought forward SPIN-E protocol which increased retransmission mechanism based on SPIN, it can be applied to network of loss. And then, the paper were using colored Petri Net to model SPIN-E, and simulated the model by CPN Tools, proved that the protocol won't deadlock and has characteristics of reachability and boundedness, verified that nodes can receive the data its want in lossy network using SPIN-E.The paper verified the rooting protocol SPIN by formal method, it is in favor of comprehensively study the protocol, and prove the usability of the protocol for wireless sensor networks, and also can find the problems in the protocol. This is significant for the improvement and development of the protocol.