无线传感器网络（WSN，Wireless Sensor Network）的应用越来越广泛，例如在火警预报、环境监测、燃气抄表等领域提供了便捷性和安全性保证，对人们的生活影响很大。数据收集是无线传感器网络主要的功能，随着数据收集协议在不同领域里的应用越来越广泛对数据收集协议分析的技术也越来越受到重视。本文针对数据收集协议的实时性需求，提出了基于UPPAAL实时模型检查器的WSN数据收集协议建模与分析方法。UPPAAL是基于时间自动机理论的、由奥尔堡大学和乌普萨拉大学联合开发的模型检查工具。由于UPPAAL的输入模型比较复杂，包括迁移时间约束、状态停留时间约束、时间自动机的交互通信等，普通用户很难直接准确建模UPPAAL的输入模型。本文针对这个问题，提出两阶段建模方法：首先对所选数据收集协议的通信行为进行时间自动机建模，进一步细化为UPPAAL的输入模型。为了阐明该方法的有效性，本文选择一个实际无线抄表数据收集协议RMT作为例子进行建模，利用UPPAAL分析其性质，并开发支持自动化分析的工具。本文主要的贡献有：（1）提出WSN数据收集协议的建模与分析方法：首先建模时间自动机模型，进而细化为UPPAAL输入模型。（2）利用提出的方法对实际无线抄表数据收集协议RMT进行形式化建模与性质分析。（3）开发工具，支持RMT协议的自动验证以及优化。