计算机科学 ›› 2016, Vol. 43 ›› Issue (9): 124-130.doi: 10.11896/j.issn.1002-137X.2016.09.024

• 网络与通信 • 上一篇    下一篇

基于UPPAAL的WSNs数据收集协议的建模与分析

冯亚超,杨红丽,王非,武文佳,秦胜潮   

  1. 北京工业大学计算机学院 北京100124,北京工业大学计算机学院 北京100124,北京工业大学计算机学院 北京100124,北京工业大学计算机学院 北京100124,北京工业大学计算机学院 北京100124;提赛德大学计算机学院 米德尔斯堡TS1 3BA
  • 出版日期:2018-12-01 发布日期:2018-12-01

Modeling and Analyzing of WSNs Data Gathering Protocol Based on UPPAAL

FENG Ya-chao, YANG Hong-li, WANG Fei, WU Wen-jia and QIN Sheng-chao   

  • Online:2018-12-01 Published:2018-12-01

摘要: 无线传感器网络(Wireless Sensor Networks,WSNs)广泛应用于各类数据收集系统,如居民区无线抄表(包括水表、电表和燃气表)系统。数据收集协议设计的正确性与合理性是影响网络正常运作的关键因素。针对数据收集协议的实时性需求,提出了基于UPPAAL实时模型检查器的WSNs数据收集协议的建模与分析方法。由于UPPAAL的输入模型相对于一般时间自动机模型而言较为复杂,因此首先对所选数据收集协议的通信行为建立一般时间自动机模型,之后再将其进一步转换为UPPAAL的输入模型。为了阐明该方法的有效性,选择了一个实际的无线抄表数据收集协议WM2RP作为例子进行建模,并利用UPPAAL分析其性质。分析结果显示,该协议能够满足一些与安全性及可靠性相关的性质。为了从多角度对协议进行分析,进一步建立了WM2RP协议的异常模型和能耗模型。

关键词: 无线传感器网络,数据收集协议,时间自动机,UPPAAL模型,建模与分析

Abstract: Wireless Sensor Networks is widely used in various types of data gathering systems,such as residential wireless meter reading (including water,electricity and gas meters) systems.The correctness and rationality of the designing of data gathering protocol are the key factors affecting the normal operation of the network.We proposed the method of modeling and analyzing of WSNs data gathering protocol based on UPPAAL towards the demand of real-time feature.Considering the input model of UPPAAL is more complex than the general terms of automata model,we established the general terms of time automata model of data gathering protocol at first,and then transfered it to the input model of UPPAAL.The effectiveness of the method is illustrated by modeling and analyzing for an actual wireless meter reading data gathering protocol WM2RP.The result shows some properties which are related to the safety and reliability can be satisfied on the protocol.The exception model and energy consumption model of WM2RP are further established to analyze the protocol from the multiple angle.

Key words: Wireless sensor networks,Data gathering protocol,Timed automata,UPPAAL model,Modeling and analyzing

[1] Zhang F J,Peng Z,Qi Y F.Research progress on Wireless Sensor Networks[J].Modern Agricultural Science and Technology,2010,1:16-17(in Chinese) 张付杰,彭争,齐亚峰.无线传感器网络研究进展[J].现代农业科技,2010,1:16-17
[2] Ren F Y,Huang H N,Lin C.Wireless Sensor Networks[J].Journal of Software,2003,14(7):1282-1291(in Chinese) 任丰原,黄海宁,林闯.无线传感器网络[J].软件学报,2003,14(7):1282-1291
[3] Xie H P,Zhou H Y,Zuo D C,et al.Energy optimization and modeling in Wireless Sensor Networks:a survey[J].Computer Science,2012,39(10):15-20(in Chinese) 谢和平,周海鹰,左德承,等.无线传感器网络能量优化与建模技术综述[J].计算机科学,2012,39(10):15-20
[4] Li L,Li J.Research of compressed sensing theory in WSN data fusion[C]∥Fourth International Symposium on Computational Intelligence and Design.Hangzhou,China:IEEE,2011,2:125-128
[5] Akkaya K,Younis M.A survey on routing protocols for Wireless Sensor Networks[J].Ad Hoc Networks,2005,3(3):325-349
[6] Ma C M,Wang W L,Hong Z.Improced Energy Efficient Data Gathering Protocol in Wireless Sensor Network[J].Computer Science,2015,42(2):65-69(in Chinese) 马晨明,王万良,洪榛.无线传感器网络中一种改进的能效数据收集协议[J].计算机科学,2015,42(2):65-69
[7] Imran M,Said A M,Hasbullah H.A survey of simulators,emulators and testbeds for Wireless Sensor Networks[J].Information Technology,Bandar Seri Iskandar,Malaysia:IEEE,2010,6(2):897-902
[8] Elleuch M,Hasan O,Tahar S,et al.Formal analysis of a scheduling algorithm for Wireless Sensor Networks[C]∥13th International Conference on Formal Engineering Methods,ICFEM 2011.Durham,UK,2011:388-403
[9] Zhou Q L,Zhang B,Xi L.System survivability analysis based on model checking[J].Computer Engineering,2012,38(17):38-41(in Chinese) 周清雷,张兵,席琳.基于模型检测的系统生存性分析[J].计算机工程,2012,38(17):38-41
[10] Behrmann G,David A,Larsen K G.A tutorial on Uppaal[M]∥Formal Methods for the Design of Real-Time Systems:Lecture Notes in Computer Science.2004:200-236
[11] Guo Z L,Gao C H,Ma L C,et al.Formal Verification of Safety Computer Platform Based on Timed Automata Model[J].Journal of the China Railway Society,2011,33(6):69-73(in Chinese) 郭志良,郜春海,马连川,等.基于时间自动机模型的安全计算机平台的形式化验证[J].铁道学报,2011,33(6):69-73
[12] Saghar K,Henderson W,Kendall D,et al.Applying formal mo-delling to detect DoS attacks in wireless medium[C]∥CSNDSP.2010
[13] Wu N.Modelling and analysis of Wireless Sensor Networks with energy harvesting capabilities[C]∥Informatics and Mathematical Modelling.2012
[14] Heinzelman W,Chandrakasan A,Balakrishnan H.Energy-Efficient cornrnunication protocol for wireless micro sensor networks[C]∥Proe.of the 33rd Annual Hawaii Int’1 Conf.on System Sciences.Maui:IEEE,2000:3005-3014
[15] Bengtsson J,Wang Y.Timed automata:semantics,algorithms and tools[M]∥Lectures on Concurrency and Petri Nets:Advances in Petri Nets.2004:87-124

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!