Sciweavers

Share
FM
2009
Springer

Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks

9 years 8 months ago
Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks
We study a clock synchronization protocol for the Chess WSN. First, we model the protocol as a network of timed automata and verify various instances using the Uppaal model checker. Next, we present a full parametric analysis of the protocol for the special case of cliques (networks with full connectivity), that is, we give constraints on the parameters that are both necessary and sufficient for correctness. These results have been checked using the proof assistant Isabelle. Finally, we present a negative result for the special case of line topologies: for any instantiation of the parameters, the protocol will eventually fail if the network grows. This result suggests a variation of the fundamental result of Fan and Lynch on gradient clock synchronization, where the synchronization eventually fails as the network diameter grows, for a setting with logical clocks whose value may also decrease. Key words: industrial application, clock synchronization, timed automata, model checking, theo...
Faranak Heidarian, Julien Schmaltz, Frits W. Vaand
Added 24 Jul 2010
Updated 24 Jul 2010
Type Conference
Year 2009
Where FM
Authors Faranak Heidarian, Julien Schmaltz, Frits W. Vaandrager
Comments (0)
books