Modelling Clock Synchronization in the Chess gMAC WSN Protocol
Logic in Computer Science2009-12-11v1Distributed, Parallel, and Cluster ComputingFormal Languages and Automata TheoryNetworking and Internet Architecture
We present a detailled timed automata model of the clock synchronization algorithm that is currently being used in a wireless sensor network (WSN) that has been developed by the Dutch company Chess. Using the Uppaal model checker, we establish that in certain cases a static, fully synchronized network may eventually become unsynchronized if the current algorithm is used, even in a setting with infinitesimal clock drifts.
Cite
@article{arxiv.0912.1901,
title = {Modelling Clock Synchronization in the Chess gMAC WSN Protocol},
author = {Mathijs Schuts and Feng Zhu and Faranak Heidarian and Frits Vaandrager},
journal= {arXiv preprint arXiv:0912.1901},
year = {2009}
}