Modeling and Evaluation of Wireless Sensor Network Protocols by Stochastic Timed Automata
Modeling and Evaluation of Wireless Sensor Network Protocols by Stochastic Timed Automata
复制标题
DOI：
10.1016/j.entcs.2013.09.001
复制
发表时间：
2013-08
影响因子：
--
通讯作者：
Fengling Zhang;Lei Bu;Linzhang Wang;Jianhua Zhao;Xin Chen;Tian Zhang;Xuandong Li
中科院分区：
文献类型：
--
作者：
Fengling Zhang;Lei Bu;Linzhang Wang;Jianhua Zhao;Xin Chen;Tian Zhang;Xuandong Li
无线传感器网络(WSNs)广泛应用于各种环境中。它们可能会遇到大量的随机不确定性和扰动，如消息丢失和节点动态。因此，保证无线传感器网络底层协议的正确性并评估其在不同环境下的性能至关重要。提出了一种基于随机时间自动机和统计模型检验的无线传感器网络协议分析和评估方法，该方法可以用经典的时间自动机对无线传感器网络的工作流程进行建模。然后，为了对现实环境中常见的消息丢失和节点动态等不确定性进行建模，可以通过随机变迁对时间自动机进行扩展，从而得到随机时间自动机。对于分析，协议的正确性可以通过时间自动机上的经典模型检测来回答，而协议在现实环境中的性能可以通过对随机模型的统计模型检测来评估。为了说明本文提出的建模和验证方法的可行性和可扩展性，本文将对传感器网络的定时同步协议(TPSN)进行全面的研究。
Wireless Sensor Networks (WSNs) are widely used in different kinds of environments. They may encounter lots of stochastic uncertainties and disturbances like message loss and node dynamics. Thus, it is critical to ensure the correctness of low level protocols in WSNs and evaluate their performance under different circumstances. In this paper, we propose a new method to analyze and evaluate WSN protocols based on stochastic timed automata and statistical model checking.For modeling, the work flow of a WSN protocol can be modeled with classical timed automata. Then, to model the uncertainties such as message loss and node dynamics, which are common in realistic circumstances, the timed automata can be extended by stochastic transitions, resulting in the stochastic timed automata. For analysis, the correctness of the protocol can be answered by classical model checking on the timed automata, while the performance of the protocol under realistic environments can be evaluated by statistical model checking on the stochastic model. To illustrate the feasibility and scalability of the modeling and verification method presented in this paper, Timing-sync Protocol for Sensor Networks (TPSN) will be studied completely throughout the paper.