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

Research of Automatic Verification Method about Radio Frequency Identification Protocol

作　　者：宋岚[1,2,3] 薛锦云[3] 胡启敏[3] 谢武平[1,3] 江东明[1,3] 游珍[3] 

机构地区：[1]武汉大学计算机学院软件工程国家重点实验室,武汉430072 [2]华东交通大学信息工程学院,南昌330013 [3]江西师范大学国家网络化支撑软件国际合作基地,南昌330022

出　　处：《计算机科学》2017年第9期99-104,共6页Computer Science

基　　金：国家自然科学基金(61272075;61472167;61462041;61363012);江西省科技厅项目(20161BBH80039)资助

摘　　要：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.

关 键 词：POPULATION Protocols RFID 协议验证 SPIN 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]