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

Modeling and Analyzing of WSNs Data Gathering Protocol Based on UPPAAL

作　　者：冯亚超 杨红丽[1] 王非[1] 武文佳[1] 秦胜潮[1,2] 

机构地区：[1]北京工业大学计算机学院,北京100124 [2]提赛德大学计算机学院

出　　处：《计算机科学》2016年第9期124-130,共7页Computer Science

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

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

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