无线传感网是由部署在监测区域的传感器节点自组织构成的网络，正确可靠的网络协议是该网络自组织高效运行的基础。在无线传感网自组织协议验证手段中，模型检验是一种形式化自动验证技术，可更加完备地探索系统行为，发现难以发现的错误，在一定程度上弥补测试实验和仿真模拟的不足。本文建立面向无线传感网自组织协议的时间自动机模型，将自组织看做汇聚节点和传感器节点协作通信的过程，使用时间自动机语义对其进行描述，并将时间自动机扩展为七元组，采用概率权值函数来描述传感网的非确定性。在上述时间自动机模型基础上，本文对基于竞争的无线传感网MAC协议CSMA/CA进行验证与分析，在时间自动机模型中加入能量消耗模型和概率验证手段，考虑到使用能量采集技术为传感器节点提供能源，建立不同的能量模型，对该协议进行了性能分析。本文还设计了一种基于QoS的路由协议GRAC，建立时间自动机模型对该协议进行验证与分析，该协议利用Dijkstra算法选择最小代价路径作为数据传输路径，使用确认和重传机制来保证数据可靠传输。本文的工作表明基于模型检测的验证与分析有助于提高无线传感网自组织协议的正确性和可靠性。