无线传感器网络(Wireless Sensor Network,简称WSN)的研究起源于军事领域,随着人类发展需要,目前它在军事、医疗保健、智能家居、环境监测、工业生产和商业领域都发挥着其重要的应用价值。就无线传感网络而言,大多数情况下需要时间同步机制。时间同步协议能为网络节点的本地时间提供共同的时间戳,为传感节点间的感知,通信,能量管理等功能提供前提条件。由于协议在设计过程中,往往比较复杂,一点错误都有可能引起整个系统故障或者数据传输错误。对协议的安全性,可靠性以及环境适用性的分析一直是协议验证的主要内容。模型检测是一种适用于协议性能验证的有效的在形式化方法。本文采用基于时间自动机的模型检测工具Uppaal对WSN的两种经典的时间同步协议(TPSN和FTSP)进行模型构建。从它们的建模流程中,本文确定了一种用于分析无线传感器协议网络的建模方法。即在分析的过程中把协议分成主要的几个部分,然后再从底层开始建模,根据具体的协议内容对模型进行扩展,最后组合成完整的时间自动机模型。从对TPSN和FTSP的原理分析中,可以确定TPSN的流程主要分为两个阶段,分层阶段和同步阶段。第二个协议FTSP在执行时,根据流程可以确定它也是由两个主要的局部模型构成,发送和接收过程。每个协议的局部模型构建是之后为其添加特殊情况建模的实现基础。本文检测了两种协议的正确性、安全性、活性。其中,TPSN在这三方面都表现正确;FTSP在性质方面没有满足,根据这个结果可以进一步分析出现问题的原因。另外,本文还拓展出协议的代价时间自动机。对一定数量的传感器节点,在一定时间段内,统计了两种协议的节点在不同环境下的同步数据。实验结果能较好的说明这两个时间同步协议不同的特点,以及各自的适用环境。同时也对它们的安全性和可靠性给出了证据。