| 基于UPPAAL的WSNs数据收集协议的建模与分析 |
| |
| 引用本文： | 冯亚超,杨红丽,王非,武文佳,秦胜潮.基于UPPAAL的WSNs数据收集协议的建模与分析[J].计算机科学,2016,43(9):124-130. |
| |
| 作者姓名： | 冯亚超 杨红丽 王非 武文佳 秦胜潮 |
| |
| 作者单位： | 北京工业大学计算机学院 北京100124,北京工业大学计算机学院 北京100124,北京工业大学计算机学院 北京100124,北京工业大学计算机学院 北京100124,北京工业大学计算机学院 北京100124;提赛德大学计算机学院 米德尔斯堡TS1 3BA |
| |
| 摘 要： | 无线传感器网络(Wireless Sensor Networks,WSNs)广泛应用于各类数据收集系统,如居民区无线抄表(包括水表、电表和燃气表)系统。数据收集协议设计的正确性与合理性是影响网络正常运作的关键因素。针对数据收集协议的实时性需求,提出了基于UPPAAL实时模型检查器的WSNs数据收集协议的建模与分析方法。由于UPPAAL的输入模型相对于一般时间自动机模型而言较为复杂,因此首先对所选数据收集协议的通信行为建立一般时间自动机模型,之后再将其进一步转换为UPPAAL的输入模型。为了阐明该方法的有效性,选择了一个实际的无线抄表数据收集协议WM2RP作为例子进行建模,并利用UPPAAL分析其性质。分析结果显示,该协议能够满足一些与安全性及可靠性相关的性质。为了从多角度对协议进行分析,进一步建立了WM2RP协议的异常模型和能耗模型。
|
| 关 键 词： | 无线传感器网络 数据收集协议 时间自动机 UPPAAL模型 建模与分析 |
| 收稿时间： | 3/9/2015 12:00:00 AM |
| 修稿时间： | 2015/7/19 0:00:00 |
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.Modeling and Analyzing of WSNs Data Gathering Protocol Based on UPPAAL[J].Computer Science,2016,43(9):124-130. |
| |
| Authors: | FENG Ya-chao YANG Hong-li WANG Fei WU Wen-jia and QIN Sheng-chao |
| |
| Affiliation: | College of Computer,Beijing University of Technology,Beijing 100124,China,College of Computer,Beijing University of Technology,Beijing 100124,China,College of Computer,Beijing University of Technology,Beijing 100124,China,College of Computer,Beijing University of Technology,Beijing 100124,China and College of Computer,Beijing University of Technology,Beijing 100124,China;College of Computer,Teeside University,Middlesbrough TS1 3BA,UK |
| |
| 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. |
| |
| Keywords: | Wireless sensor networks Data gathering protocol Timed automata UPPAAL model Modeling and analyzing |
|
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
