×

Analysis of a clock synchronization protocol for wireless sensor networks. (English) Zbl 1307.68009

Summary: The Dutch company Chess develops a wireless sensor network (WSN) platform using an epidemic communication model. One of the greatest challenges in the design is to find suitable mechanisms for clock synchronization. In this paper, we study a proposed clock synchronization protocol for the Chess platform. 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. We report on the exhaustive analysis of the protocol for networks with four nodes, and 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.

MSC:

68M14 Distributed systems
68M10 Network design and communication in computer systems
68M12 Network protocols
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Heidarian, F.; Schmaltz, J.; Vaandrager, F., Analysis of a clock synchronization protocol for wireless sensor networks, (Cavalcanti, A.; Dams, D., Proceedings 16th International Symposium of Formal Methods. Proceedings 16th International Symposium of Formal Methods, FM2009, Eindhoven, the Netherlands, November 2-6. Proceedings 16th International Symposium of Formal Methods. Proceedings 16th International Symposium of Formal Methods, FM2009, Eindhoven, the Netherlands, November 2-6, Lecture Notes in Computer Science, vol. 5850 (2009), Springer), 516-531, URL: http://www.mbsd.cs.ru.nl/publications/papers/fvaan/HSV09/
[2] QUASIMODO, Case studies: Models, deliverable 5.5 from the FP7 ICT STREP project 214755 (QUASIMODO), Jan. 2009. URL: http://www.quasimodo.aau.dk/Final/Deliverable-5.5.pdf; QUASIMODO, Case studies: Models, deliverable 5.5 from the FP7 ICT STREP project 214755 (QUASIMODO), Jan. 2009. URL: http://www.quasimodo.aau.dk/Final/Deliverable-5.5.pdf
[3] QUASIMODO, Preliminary description of case studies, deliverable 5.2 from the FP7 ICT STREP project 214755 (QUASIMODO), Jan. 2009. URL: http://www.quasimodo.aau.dk/Final/Deliverable-5.2.pdf; QUASIMODO, Preliminary description of case studies, deliverable 5.2 from the FP7 ICT STREP project 214755 (QUASIMODO), Jan. 2009. URL: http://www.quasimodo.aau.dk/Final/Deliverable-5.2.pdf
[4] Kermarrec, A.-M.; Steen, M.v., Gossiping in distributed systems, SIGOPS Oper. Syst. Rev., 41, 5, 2-7 (2007), doi: http://doi.acm.org/10.1145/1317379.1317381
[5] Demers, A.; Greene, D.; Hauser, C.; Irish, W.; Larson, J.; Shenker, S.; Sturgis, H.; Swinehart, D.; Terry, D., Epidemic algorithms for replicated database maintenance, (PODC ’87: Proceedings of the sixth annual ACM Symposium on Principles of distributed computing (1987), ACM: ACM New York, NY, USA), 1-12, doi: http://doi.acm.org/10.1145/41840.41841
[6] Bakhshi, R.; Bonnet, F.; Fokkink, W.; Haverkort, B., Formal analysis techniques for gossiping protocols, SIGOPS Oper. Syst. Rev., 41, 5, 28-36 (2007), doi: http://doi.acm.org/10.1145/1317379.1317385
[7] F. Assegei, Decentralized frame synchronization of a TDMA-based wireless sensor network, Master’s Thesis, Eindhoven University of Technology, Department of Electrical Engineering, 2008.; F. Assegei, Decentralized frame synchronization of a TDMA-based wireless sensor network, Master’s Thesis, Eindhoven University of Technology, Department of Electrical Engineering, 2008.
[8] Sundararaman, B.; Buy, U.; Kshemkalyani, A. D., Clock synchronization for wireless sensor networks: a survey, Ad Hoc Netw., 3, 3, 281-323 (2005), doi:. URL: http://www.sciencedirect.com/science/article/B7576-4FDMVS4-1/2/63ed40b032c6bf3ad5fca7fdcbe9e35a
[9] Fan, R.; Lynch, N., Gradient clock synchronization, Distrib. Comput., 18, 4, 255-266 (2006) · Zbl 1266.68049
[10] Lamport, L., Time, clocks and the ordering of events in distributed systems, Commun. ACM, 21, 7, 558-564 (1978) · Zbl 0378.68027
[11] L. Meier, L. Thiele, Gradient clock synchronization in sensor networks, Tech. Rep. 219, Computer Engineering and Networks Laboratory, ETH Zurich, 2005.; L. Meier, L. Thiele, Gradient clock synchronization in sensor networks, Tech. Rep. 219, Computer Engineering and Networks Laboratory, ETH Zurich, 2005.
[12] Pussente, R.; Barbosa, V., An algorithm for clock synchronization with the gradient property in sensor networks, J. Parallel Distrib. Comput., 69, 3, 261-265 (2009), doi:. URL: http://www.sciencedirect.com/science/article/B6WKJ-4TYJTY5-1/2/38716d7d9f37c51edb8ba05e508fa2ce
[13] R. Tjoa, K. Chee, P. Sivaprasad, S. Rao, J. Lim, Clock drift reduction for relative time slot tdma-based sensor networks, in: Proceedings of the 15th IEEE International Symposium on Personal, Indoor and Mobile Radio Communications, PIMRC2004, 2004, pp. 1042-1047.; R. Tjoa, K. Chee, P. Sivaprasad, S. Rao, J. Lim, Clock drift reduction for relative time slot tdma-based sensor networks, in: Proceedings of the 15th IEEE International Symposium on Personal, Indoor and Mobile Radio Communications, PIMRC2004, 2004, pp. 1042-1047.
[14] Schuts, M.; Zhu, F.; Heidarian, F.; Vaandrager, F., Modelling clock synchronization in the Chess gMAC WSN protocol, (S. A.; etal., Proceedings Workshop on Quantitative Formal Methods: Theory and Applications, QFM’09. Proceedings Workshop on Quantitative Formal Methods: Theory and Applications, QFM’09, Electronic Proceedings in Theoretical Computer Science, vol. 13 (2009)), 41-54, URL: http://www.mbsd.cs.ru.nl/publications/papers/fvaan/chess09/
[15] F. Heidarian, A comment on Assegei’s use of Kalman filters for clock synchronization, iCIS, Radboud University Nijmegen. Available at http://www.mbsd.cs.ru.nl/publications/papers/fvaan/HSV09/; F. Heidarian, A comment on Assegei’s use of Kalman filters for clock synchronization, iCIS, Radboud University Nijmegen. Available at http://www.mbsd.cs.ru.nl/publications/papers/fvaan/HSV09/
[16] QUASIMODO, Final report: case studies and tool integration, deliverable 5.10 from the FP7 ICT STREP project 214755 (QUASIMODO), April 2011. URL: http://www.quasimodo.aau.dk/Final/Deliverable-5.10.pdf; QUASIMODO, Final report: case studies and tool integration, deliverable 5.10 from the FP7 ICT STREP project 214755 (QUASIMODO), April 2011. URL: http://www.quasimodo.aau.dk/Final/Deliverable-5.10.pdf
[17] Behrmann, G.; David, A.; Larsen, K., A tutorial on Uppaal, (Bernardo, M.; Corradini, F., Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems. Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures. Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems. Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures, Lecture Notes in Computer Science, vol. 3185 (2004), Springer), 200-236 · Zbl 1105.68350
[18] Behrmann, G.; David, A.; Larsen, K. G.; Håkansson, J.; Pettersson, P.; Yi, W.; Hendriks, M., Uppaal 4.0, (Third International Conference on the Quantitative Evaluation of SysTems, QEST 2006. Third International Conference on the Quantitative Evaluation of SysTems, QEST 2006, 11-14 September 2006, Riverside, CA, USA (2006), IEEE Computer Society), 125-126
[19] Nipkow, T.; Paulson, L.; Wenzel, M., (Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer) · Zbl 0994.68131
[20] F. Wiedijk, The de Bruijn factor, webpage accessed October 2010. http://www.cs.ru.nl/ freek/factor/; F. Wiedijk, The de Bruijn factor, webpage accessed October 2010. http://www.cs.ru.nl/ freek/factor/
[21] Bruijn, N.d., A survey of the project Automath, (Hindley, J.; Seldin, J., To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalisms (1980), Academic Press)
[22] QUASIMODO, Dissemination and exploitation, deliverable 5.6 from the FP7 ICT STREP project 214755 (QUASIMODO), Feb. 2010. URL: http://www.quasimodo.aau.dk/Final/Deliverable-5.6.pdf; QUASIMODO, Dissemination and exploitation, deliverable 5.6 from the FP7 ICT STREP project 214755 (QUASIMODO), Feb. 2010. URL: http://www.quasimodo.aau.dk/Final/Deliverable-5.6.pdf
[23] Cavin, D.; Sasson, Y.; Schiper, A., On the accuracy of manet simulators, (Proceedings of the 2002 Workshop on Principles of Mobile Computing. Proceedings of the 2002 Workshop on Principles of Mobile Computing, POMC 2002, October 30-31, 2002, Toulouse, France (2002), ACM), 38-43
[24] Vaandrager, F.; Groot, A.d., Analysis of a biphase mark protocol with Uppaal and PVS, Formal Aspects Comput. J., 18, 4, 433-458 (2006), doi: http://dx.doi.org/10.1007/s00165-006-0008-1. URL: http://www.ita.cs.ru.nl/publications/papers/fvaan/BMP.html · Zbl 1102.68505
[25] Rushby, J., A formally verified algorithm for clock synchronization under a hybrid fault model, (PODC ’94: Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing (1994), ACM: ACM New York, NY, USA), 304-313, doi: http://doi.acm.org/10.1145/197917.198115 · Zbl 1373.68143
[26] Schmaltz, J., A formal model of clock domain crossing and automated verification of time-triggered hardware, (Baumgartner, J.; Sheeran, M., Formal Methods in Computer Aided Design (2007), IEEE Computer Society), 223-230, URL: http://doi.ieeecomputersociety.org/10.1109/FMCAD.2007.2
[27] Brown, G. M.; Pike, L., Easy parameterized verification of biphase mark and 8N1 protocols, (Hermanns, H.; Palsberg, J., TACAS. TACAS, Lecture Notes in Computer Science, vol. 3920 (2006), Springer), 58-72
[28] Umeno, S., Event order abstraction for parametric real-time system verification, (de Alfaro, L.; Palsberg, J., EMSOFT (2008), ACM), 1-10
[29] A. Carioni, S. Ghilardi, S. Ranise, MCMT in the land of parameterized timed automata, in: J. Giesl, R. Hähnle (Eds.), 6th International Verification Workshop, VERIFY 2010, associated with IJCAR, Edinburgh, UK, July 20-21, 2010. Proceedings, 2010. Available at http://homes.dsi.unimi.it/ ghilardi/allegati/verify.pdf; A. Carioni, S. Ghilardi, S. Ranise, MCMT in the land of parameterized timed automata, in: J. Giesl, R. Hähnle (Eds.), 6th International Verification Workshop, VERIFY 2010, associated with IJCAR, Edinburgh, UK, July 20-21, 2010. Proceedings, 2010. Available at http://homes.dsi.unimi.it/ ghilardi/allegati/verify.pdf
[30] Ghilardi, S.; Ranise, S., MCMT: A model checker modulo theories, (Giesl, J.; Hähnle, R., Automated Reasoning, 5th International Joint Conference. Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings. Automated Reasoning, 5th International Joint Conference. Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6173 (2010), Springer), 22-29 · Zbl 1291.68257
[31] Kwiatkowska, M.; Norman, G.; Parker, D., PRISM 2.0: A tool for probabilistic model checking, (Proceedings of the 1st International Conference on Quantitative Evaluation of Systems, QEST04 (2004), IEEE Computer Society), 322-323
[32] Fehnker, A.; Fruth, M.; McIver, A., Graphical modelling for simulation and formal analysis of wireless network protocols, (Butler, M.; Jones, C.; Romanovsky, A.; Troubitsyna, E., Methods, Models and Tools for Fault Tolerance. Methods, Models and Tools for Fault Tolerance, Lecture Notes in Computer Science, vol. 5454 (2009), Springer), 1-24
[33] Bakhshi, R.; Cloth, L.; Fokkink, W.; Haverkort, B., Mean-field analysis for the evaluation of gossip protocols, (QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems. QEST 2009, Sixth International Conference on the Quantitative Evaluation of Systems, Budapest, Hungary, 13-16 September 2009 (2009), IEEE Computer Society), 247-256
[34] Fehnker, A.; van Hoesel, L.; Mader, A., Modelling and verification of the lmac protocol for wireless sensor networks, (Davies, J.; Gibbons, J., Integrated Formal Methods, 6th International Conference. Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings. Integrated Formal Methods, 6th International Conference. Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4591 (2007), Springer), 253-272
[35] Tschirner, S.; Xuedong, L.; Yi, W., Model-based validation of qos properties of biomedical sensor networks, (de Alfaro, L.; Palsberg, J., Proceedings of the 8th ACM & IEEE International conference on Embedded software. Proceedings of the 8th ACM & IEEE International conference on Embedded software, EMSOFT 2008, Atlanta, GA, USA, October 19-24, 2008 (2008), ACM), 69-78
[36] Woehrle, M.; Lampka, K.; Thiele, L., Exploiting timed automata for conformance testing of power measurements, (Ouaknine, J.; Vaandrager, F. W., Formal Modeling and Analysis of Timed Systems, 7th International Conference. Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings. Formal Modeling and Analysis of Timed Systems, 7th International Conference. Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5813 (2009), Springer), 275-290, doi: http://dx.doi.org/10.1007/978-3-642-04368-0. URL: http://dx.doi.org/10.1007/978-3-642-04368-0
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.