Computer Science ›› 2017, Vol. 44 ›› Issue (9): 99-104.doi: 10.11896/j.issn.1002-137X.2017.09.020

Previous Articles     Next Articles

Research of Automatic Verification Method about Radio Frequency Identification Protocol

SONG Lan, XUE Jin-yun, HU Qi-min, XIE Wu-ping, JIANG Dong-ming and YOU Zhen   

  • Online:2018-11-13 Published:2018-11-13

Abstract: 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-collision 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.

Key words: Population Protocols,RFID,Protocol verification,Spin

[1] SHAHZAD M,LIU AX.Probabilistic optimal tree hopping for RFID identification[J].ACM Sigmetrics Performance Evaluation Review,2013,1(1):293-304.
[2] DIJKSTRA E W.Self-stabilization in spite of distributed control[C]∥Selected Writing on Computing:A personal Perspective.Springer-Verlag,Berlin,1982:41-46.
[3] ANGLUI D,ASPNES J,DIAMADI Z,et al.Computation in networks of passively mobile finite-state sensors[J].Distributed Computing,2006,8(4):235-253.
[4] ALISTARH D,ASPNES J,EISENSTAT D.Time-space trade-offs in population protocols[EB/OL].[2016-02-25].https://www.researchgate.net.
[5] ASPNES J,RUPPERT E.An introduction to population protocols[C]∥Middleware for Network Eccentric and Mobile Applications.Heidelberg:Springer,2009:97-120.
[6] PANG J,LUO Z,DENG Y.On automatic verification of self-stabilizing population protocols[J].Frontiers of Computer Science in China,2008,2(4):185-192.
[7] JIANG H.Distributed system of simple interacting agents[D].Connecticut:Yale University,2007.
[8] CLEMENT J,DELPORTE-GALLET C,FAVCONNIER H,et al.Guidelines for the verification of population protocols[C]∥2011 31st International Conference on Distributed Computing Systems.Minneapolis:ACM,2011:215-224.
[9] LIU Y.Model checking concurrent and read-time systems:the PAT approach[D].Singapore:Computer science national university of Singapore,2009.
[10] MERY D,POPPLETON M.Formal modeling and verification of population protocols[M]∥Lecture Notes in Computer Science.Turku:Springer,2013:208-222.
[11] BECCHETTI L,BERGAMINI L,FICAROLA F,et al.Population Protocols on real social networks[C]∥Proceedings of the 9th ACM Symposium on Performance Evaluation of Wireless Adhoc,Sensor,and Ubiquitous Networks.Minneapolis:ACM,2012:17-24.
[12] PENNISI A,PREVITALI F,FICAROLA F,et al.Distributedsensor network for multi_robot surveillance[C]∥3rd International Workshop on Cooperative Robots and Sensor Networks(Robosense-2014).Amsterdam:Elsevier,2014:1095-1100.
[13] KOMU B N,MZYECE M,DJOUANI K.Spin-based verification of authentication protocols in WiMAX networks[C]∥2012 Vehicular Technology Conference(VTC Fall).IEEE,2012:1-5.
[14] FENG J.Formal analysis and verification of SPIN protocol[D].Guizhou:Guizhou University,2009.(in Chinese) 冯杰.基于SPIN的协议的形式化分析和验证[D].贵州:贵州大学,2009.
[15] 古天龙,蔡国永.网络协议的形式化分析与设计[M].北京:电子工业出版社,2003:37-80.
[16] 吴哲辉.Petri网导论[M].北京:机械工业出版社,2006:10-30.
[17] 原菊梅.Petri网建模及其智能分析方法[M].北京:国防工业出版社,2011:39-122.
[18] HOLZMANN G J.The spin model checker:primer and referen-ce manual[M].New Jersey:Addison-Wesley,2003:95-123.

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!