随着无线传感器技术的发展,无线传感器网络(Wireless Sensor Network,WSN)得到极大的关注。WSN有着广泛的应用场景,在一些危险、不易到达以及不易生存等情景下,利用无线传感器(Wireless Sensor)代替人去监测、控制目标成为自然而然的选择。这些传感器之间的通信就必须使用WSN,为了使无线传感器能达成监测、控制目标的目的,WSN协议必须确保功能的正确性；同时无线传感器往往资源有限、能量受限,WSN协议也要考虑性能与功耗问题。为了确保功能正确性,人们通常使用测试与仿真、定理证明以及模型检测(Model Checking)技术。测试与仿真无法对系统进行全面检测,定理证明需要过多人工干预,模型检测技术是一种可以自动对系统模型进行全面分析的检测手段,故本文使用模型检测技术进行建模分析。为了对性能与功耗进行分析,本文使用统计模型检测技术(Statistical Model Checking,SMC)。传统的模型检测技术由于状态空间爆炸问题难以对复杂系统模型进行定量分析,SMC技术利用统计学与仿真手段避免了对整个系统模型状态空间的搜索,不会遇到状态空间爆炸问题,为性能与功耗的分析提供了新方法。Minimum Cost Forward(MCF)协议是WSN网络层一种重要的协议,该协议使用了基于代价的方法形成最小代价转发路径。在此过程中无需存储路由表,数据按照最小代价路径进行传输,适用于能量与资源受限的WSN。本文针对MCF协议进行建模与分析。首先重新建立了MCF协议的时间自动机(Timed Automata, TA)模型,用时间计算树逻辑(Timed Computation Tree Logic,TCTL)语言描诉了协议的安全性、活性,在模型检测器UPPAAL上进行了验证；然后根据本文建立的TA模型,用代价时间自动机(Priced Timed Automata,PTA)对链路错误以及节点失效两种情形进行了建模,并用统计模型检测的方法分析其定量属性；除此之外,本文还利用SMC技术对协议在无损通信时的功耗进行了分析。经过分析,发现在理想情形下,MCF协议可以完成WSN的路由,但是不能均衡地消耗WSN中的能量,同时在进行有损通信时,MCF协议无法有效进行数据传输。