1. Modelling Clock Synchronization in the Chess gMAC WSN Protocol
- Author
-
Schuts, M., Zhu, F., Heydarian, F., Vaandrager, F.W., Andova, Suzana, McIver, Annabelle, D'Argenio, Pedro, Cuijpers, Pieter, Markovski, Jasen, Morgan, Caroll, Nunez, Manuel, Andova, Suzana, McIver, Annabelle, D'Argenio, Pedro, Cuijpers, Pieter, Markovski, Jasen, Morgan, Caroll, and Nunez, Manuel
- Subjects
Model checking ,FOS: Computer and information sciences ,Computer Science - Logic in Computer Science ,Computer science ,Formal Languages and Automata Theory (cs.FL) ,Electronic Proceedings in Theoretical Computer Science ,Infinitesimal ,Real-time computing ,Computer Science - Formal Languages and Automata Theory ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,Clock synchronization ,lcsh:QA75.5-76.95 ,Computer Science - Networking and Internet Architecture ,0202 electrical engineering, electronic engineering, information engineering ,Software Science ,Computer Science::Networking and Internet Architecture ,Protocol (object-oriented programming) ,Networking and Internet Architecture (cs.NI) ,lcsh:Mathematics ,020206 networking & telecommunications ,lcsh:QA1-939 ,Automaton ,Logic in Computer Science (cs.LO) ,Computer Science - Distributed, Parallel, and Cluster Computing ,010201 computation theory & mathematics ,Distributed, Parallel, and Cluster Computing (cs.DC) ,lcsh:Electronic computers. Computer science ,Wireless sensor network - Abstract
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.
- Published
- 2009