无线射频RFID识别协议自动验证方法研究

Research of Automatic Verification Method about Radio Frequency Identification Protocol

Population Protocols是一种受生物启发的计算模型,能够表示无线网络中数量庞大但计算能力弱的多组件间的交互,它为无线传感器网络提供了一种可计算推理的理论框架。将Population Protocol理论引入到RFID识别协议中,提出了RFID识别协议系统模型验证框架;构建了标签与阅读器交互产生的状态变迁模型;最后用spin模型检测工具和LTL线性时序逻辑验证了弱公平条件下该模型的自稳定性,为分析与验证无线传感器网络中协议的正确性提供了一种行之有效的方法。

Population Protocols,which is a calculation model inspired by biology, was designed to represent interaction between multiple components with very limited computational capability in wireless network. It provides a theoretical framework which has the function of computation and reasoning for wireless sensor networks. This paper introduced the population protocols model into the RFID anti-collision protocol, proposed the validation framework of RFID anti-colli- sion protocol,built the state transition model through the interaction between the tag and the reader, and verified the self-stabilizing population protocols by using the spin model checker and linear temporal logic （LTL）. These work will provide us an effective method to analyze and verify the correctness of the protocol in wireless sensor networks.