Affordable Access

Publisher Website

Modeling and Evaluation of Wireless Sensor Network Protocols by Stochastic Timed Automata

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
296
Identifiers
DOI: 10.1016/j.entcs.2013.09.001
Keywords
  • Wireless Sensor Network Protocol
  • Modeling And Evaluation
  • Stochastic Timed Automata
  • Statistical Model Checking
Disciplines
  • Mathematics

Abstract

Abstract 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.

There are no comments yet on this publication. Be the first to share your thoughts.