Poster Abstract: Numerical Analysis of WSN Protocol Using Probabilistic Timed Automata

Timing-sync Protocol for Sensor Networks (TPSN) is a widely used protocol which provides network-wide time synchronization in a sensor network. We use formal methods to study it thoroughly in this poster. First of all, we model the protocol with timed automata which can describe the workflow of TPSN in an ideal environment. However, in realistic circumstances, there are many uncertainties, for example, message loss and node dynamics. Thus, we extend our model with probabilities to describe these uncertainties. Besides verifying the system against several critical functional properties, we also show that it is also possible to evaluate the performance of TPSN by statistical model checking to estimate how it works in realistic environments.