随着半导体技术、微系统技术、计算机技术、通信技术的快速发展,无线传感器网络在各个领域得到了广泛的应用,对它的研究也显得日益重要。而无线传感器网络与一般的计算机网络技术相比又有着自身独有的特点：比如节点能量很有限,要求有高效的节能措施；以数据为中心,要对冗余的数据进行融合。这些都与传统的网络只追求高传输率和高服务质量的目标差距很大。因此,针对无线传感器网络的用途和特点开发设计出了一些新的协议。但是现在对其的研究和描述都局限在自然语言下,这些方法不利于整个协议开发的统一和抽象,且不利于协议的分析和改进。运用形式化的描述和验证方法对现有的协议进行研究和改进并在其指导下开发新的协议已成为协议研究领域重要的课题之一。由于Petri网适于形式化描述,具有相关可操作性模型,并且便于进行分析与验证,因此在网络协议的实现及分析领域得到了广泛的应用。基于Petri网的协议形式化分析方法由于其精炼、简洁和无二义性逐步成为分析协议的一条可靠和准确的途径,本文首先运用P/T型Petri网作为分析工具,着重分析了HEED协议的静态特性与动态特性,其中主要有P-不变量验证,T-不变量验证,协议状态间可达关系、无死锁、序列的合法性的验证等,而后为HEED协议建立GSPN能耗模型,并对建立的能耗模型进行分析,讨论了能耗模型对协议的改进所起的指导作用。并根据GSPN模型的分析结果发现了其孤立节点不入簇所带来的性能缺陷,为协议性能的改进提供了参考且提出了改进方案。随后本文根据GSPN性能模型中发现的性能缺陷和目前的研究现状改进了HEED协议现有的簇间路由方式,提出了一种叫做簇间最小代价路由协议的新协议。该协议使一部分的孤立节点可以入簇,且设立了由两个权值映射的一个综合评价值作为代价的衡量标准,其中一个权值为离基站的距离,另外一个为剩余电量的多少,并为了防止一个簇首转发过多的数据会过早死亡而设立了一个令牌阀值,最终可以使数据层次性的从基站的远端到近端且由能量低的节点向能量高的节点流动。最后进行的仿真结果表明,该协议解决了GSPN模型中孤立节点的能耗问题,与原有的HEED协议和HEED-CHEE相比,进一步的减小了网络中节点的能耗,延长了大约15%-25%的网络生存期。