基于随机时间自动机和统计模型检验技术的无线传感网络协议建模与分析

近年来，传感器技术得到了长足而有效的提升，无线传感网络（WSN）以其开放、动态的特征获得了极大的关注，并成为了互联网计算的一个重要组成．WSN系统行为复杂，经常面临信息丢失、节点动态变化等不确定因素，且网络中的节点一旦部署将很难更改、维护．因此，为了保证相关应用的正常工作，在系统设计阶段对WSN中的底层协议进行质量保障就成为了一项非常重要的研究问题．系统设计人员不仅需要保证协议功能上的正确性，还应该评估协议在目标工作环境下的性能，以保证其可以胜任相应的工作需求．针对以上问题，本文提出了一种基于随机时间自动机和统计模型检验技术的WSN协议建模、分析和评估途径．在建模阶段，首先将采用时间自动机对协议在理想环境下的基本业务流程进行建模．考虑到WSN系统实际工作中会遇到的各种不确定性因素，将用带权分枝来对模型进行扩展，生成协议的随机时间自动机．在验证阶段，首先采用经典模型检验技术，在理想时间自动机上检验相关功能性质，保证协议工作逻辑的正确性．为评估协议在不同条件下的具体性能，则在随机时间自动机上用统计模型检验技术对其进行数值分析，以进行参数配置、性能预测、协议比较等工作．为展示该途径的可用性及其技术细节，本文对两种著名的WSN时间同步协议，TPSN和FTSP分别进行了完整的建模与评估．

Modeling and analysis of wireless sensor network protocols by stochastic timed automata and statistical model checking

Recently, sensor technology has seen significant achievement. Meanwhile, Wireless Sensor Network （WSN） technique has attracted lots of attention because of its open and dynamic behaviors, and has become a very important component of the Internet-based computing. The behavior of WSN system is very complex and may encounter lots of stochastic uncertainties and disturbances like message loss and node dynamics. Furthermore, WSN system is difficult to change and maintain once it is deployed. Thus, it is critical to ensure the quality of the low level protocols of WSN system in design phase. Designers should ensure the logical correctness of a protocol, as well as evaluate tile performance of the protocol under certain target environments. To handle these issues, in this paper, we propose a framework to analyze and evaluate WSN protocols based on stochastic timed automata and statistical model checking. We propose to address the modeling of the uncertainties in the realistic behaviors by weighted stochastic transitions in the timed automata model of the protocol, l~lrthermore, we propose that the performance of the protocol tinder realistic environments should be evaluated by statistical model checking which is much cheaper and more scalable. To illustrate the feasibility and detail of the modeling and verification approach presented in this paper, two well-known WSN protocols, Timing-sync Protocol for Sensor Networks （TPSN） and Flooding Time Synchronization Protocol （FTSP）, are studied thoroughly throughout the paper.