Date Added: Dec 2009
The authors present a detailed 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, they 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. Wireless sensor networks consist of autonomous devices that communicate via radio and use sensors to cooperatively monitor physical or environmental conditions. In this paper, they formally model and analyze a distributed algorithm for clock synchronization in wireless sensor networks that has been developed by the Dutch company Chess in the context of the MyriaNed project.