Computer Science ›› 2016, Vol. 43 ›› Issue (9): 124-130.doi: 10.11896/j.issn.1002-137X.2016.09.024

Previous Articles     Next Articles

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

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!
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .