Modelling Clock Synchronization in the Chess gMAC WSN Protocol
| Autor: | Schuts, M., Zhu, F., Heydarian, F., Vaandrager, F.W., Andova, Suzana, McIver, Annabelle, D'Argenio, Pedro, Cuijpers, Pieter, Markovski, Jasen, Morgan, Caroll, Nunez, Manuel |
|---|---|
| Přispěvatelé: | Andova, Suzana, McIver, Annabelle, D'Argenio, Pedro, Cuijpers, Pieter, Markovski, Jasen, Morgan, Caroll, Nunez, Manuel |
| Jazyk: | angličtina |
| Rok vydání: | 2009 |
| Předmět: |
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 |
| Zdroj: | Electronic Proceedings in Theoretical Computer Science, Vol 13, Iss Proc. QFM 2009, Pp 41-54 (2009) Andova, Suzana; McIver, Annabelle; D'Argenio, Pedro (ed.), Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications Eindhoven, The Netherlands, 3rd November 2009, pp. 41-54 Andova, Suzana; McIver, Annabelle; D'Argenio, Pedro (ed.), Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications Eindhoven, The Netherlands, 3rd November 2009, 41-54. S.l : EPTCS STARTPAGE=41;ENDPAGE=54;ISSN=2075-2180;TITLE=Andova, Suzana; McIver, Annabelle; D'Argenio, Pedro (ed.), Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications Eindhoven, The Netherlands, 3rd November 2009 QFM |
| ISSN: | 2075-2180 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|