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

摘要

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