近年来,传感器技术得到了长足而有效的提升,无线传感网络(WSN)以其开放、动态的特征获得了极大的关注,并成为了互联网计算的一个重要组成.WSN系统行为复杂,经常面临信息丢失、节点动态变化等不确定因素,且网络中的节点一旦部署将很难更改、维护.因此,为了保证相关应用的正常工作,在系统设计阶段对WSN中的底层协议进行质量保障就成为了一项非常重要的研究问题.系统设计人员不仅需要保证协议功能上的正确性,还应该评估协议在目标工作环境下的性能,以保证其可以胜任相应的工作需求.针对以上问题,本文提出了一种基于随机时间自动机和统计模型检验技术的WSN协议建模、分析和评估途径.在建模阶段,首先将采用时间自动机对协议在理想环境下的基本业务流程进行建模.考虑到WSN系统实际工作中会遇到的各种不确定性因素,将用带权分枝来对模型进行扩展,生成协议的随机时间自动机.在验证阶段,首先采用经典模型检验技术,在理想时间自动机上检验相关功能性质,保证协议工作逻辑的正确性.为评估协议在不同条件下的具体性能,则在随机时间自动机上用统计模型检验技术对其进行数值分析,以进行参数配置、性能预测、协议比较等工作.为展示该途径的可用性及其技术细节,本文对两种著名的WSN时间同步协议,TPSN和FTSP分别进行了完整的建模与评估. In recent years, sensor technology has been greatly and effectively improved, wireless sensor network (WSN) has attracted great attention due to its open and dynamic characteristics, and has become an important component of Internet computing.WSN system is complicated and often Faced with uncertainties such as loss of information and dynamic change of nodes, and once the nodes in the network are deployed, it is hard to change and maintain.Therefore, in order to ensure the normal operation of related applications, the quality assurance of the underlying protocols in WSN Has become a very important research problem.System designers not only need to ensure the functional correctness of the protocol, but also evaluate the performance of the protocol in the target working environment to ensure that it can be competent for the corresponding work requirements.In view of the above problems, A WSN protocol modeling, analysis and evaluation approach based on stochastic time automata and statistical model checking technology is proposed.In the modeling stage, the basic business process of protocol under the ideal environment is first modeled using time automata. Taking into account the various uncertainties encountered in the actual work of the WSN system, we will use the weighted branches to model Extend and generate protocol.At the stage of verification, we first use the classical model checking technology to test the related functional properties on the ideal time automatic machine to ensure the correctness of the protocol working logic.In order to evaluate the specific performance of the protocol under different conditions, The statistical model test technique is used to conduct numerical analysis on the random time machine to conduct parameter configuration, performance prediction, protocol comparison, etc. In order to demonstrate the availability of the approach and its technical details, two well-known WSN time synchronization Protocols, TPSNs and FTSPs have completed a complete modeling and evaluation.