zbMATH — the first resource for mathematics

Multi-scale verification of distributed synchronisation. (English) Zbl 07307311
Summary: Algorithms for the synchronisation of clocks across networks are both common and important within distributed systems. We here address not only the formal modelling of these algorithms, but also the formal verification of their behaviour. Of particular importance is the strong link between the very different levels of abstraction at which the algorithms may be verified. Our contribution is primarily the formalisation of this connection between individual models and population-based models, and the subsequent verification that is then possible. While the technique is applicable across a range of synchronisation algorithms, we particularly focus on the synchronisation of (biologically-inspired) pulse-coupled oscillators, a widely used approach in practical distributed systems. For this application domain, different levels of abstraction are crucial: models based on the behaviour of an individual process are able to capture the details of distinguished nodes in possibly heterogenous networks, where each node may exhibit different behaviour. On the other hand, collective models assume homogeneous sets of processes, and allow the behaviour of the network to be analysed at the global level. System-wide parameters may be easily adjusted, for example environmental factors inhibiting the reliability of the shared communication medium. This work provides a formal bridge across the “abstraction gap” separating the individual models and the population-based models for this important class of synchronisation algorithms.
68 Computer science
iscasMc; PRISM; Storm; Uppaal
Full Text: DOI
[1] Akyildiz, IF; Su, W.; Sankarasubramaniam, Y.; Cayirci, E., Wireless sensor networks: a survey, Comput Netw, 38, 4, 393-422 (2002)
[2] Albers, S., Energy-efficient algorithms, Commun ACM, 53, 5, 86-96 (2010)
[3] Alur, R.; Dill, DL, A theory of timed automata, Theor Comput Sci, 126, 2, 183-235 (1994) · Zbl 0803.68071
[4] Alur, R.; Henzinger, TA, Reactive modules, Form Methods Syst. Design, 15, 1, 7-48 (1999)
[5] Angluin, D.; Aspnes, J.; Diamadi, Z.; Fischer, MJ; Peralta, R., Computation in networks of passively mobile finite-state sensors, Distrib Comput, 18, 4, 235-253 (2006) · Zbl 1266.68042
[6] Atmel Corporation (2018) ATmega128L: 8-bit Atmel microcontroller with 128 kBytes in-system programmable flash. http://www.atmel.com/images/doc2467.pdf, last accessed 6th April 2018
[7] Baier, C.; Hermanns, H.; Grumberg, O., Weak bisimulation for fully probabilistic processes, Computer aided verification, 119-130 (1997), Berlin: Springer, Berlin
[8] Bartocci, E.; Corradini, F.; Merelli, E.; Tesei, L., Detecting synchronisation of biological oscillators by model checking, Theor Comput Sci, 411, 20, 1999-2018 (2010) · Zbl 1209.68311
[9] Basler G, Mazzucchi M, Wahl T, Kroening D (2009) Symbolic counter abstraction for concurrent software. In: CAV 2009, Springer, Heidelberg, LNCS, vol 5643, pp 64-78, doi:10.1007/978-3-642-02658-4_9 · Zbl 1242.68055
[10] Behrmann G, David A, Larsen KG, Hakansson J, Petterson P, Yi W, Hendriks M (2006) Uppaal 4.0. In: QEST 2006, IEEE Computer Society, pp 125-126
[11] Breza M (2013) Bio-inspired tools for a distributed wireless sensor network operating system. PhD thesis, Imperial College, London
[12] Cardelli, L.; Kwiatkowska, M.; Laurenti, L., Programming discrete distributions with chemical reaction networks, Nat Comput, 17, 1, 131-145 (2018) · Zbl 1451.68108
[13] Cardelli, L.; Kwiatkowska, M.; Whitby, M., Chemical reaction network designs for asynchronous logic circuits, Nat Comput, 17, 1, 109-130 (2018) · Zbl 1451.68109
[14] Chen, Z.; Zhang, D.; Zhu, R.; Ma, Y.; Yin, P.; Xie, F., A review of automated formal verification of ad hoc routing protocols for wireless sensor networks, Sensor Lett, 11, 5, 752-764 (2013)
[15] Christensen, AL; Grady, RO; Dorigo, M., From fireflies to fault-tolerant swarms of robots, IEEE Trans Evolut Comput, 13, 4, 754-766 (2009)
[16] Cristian, F., Probabilistic clock synchronization, Distrib Comput, 3, 3, 146-158 (1989) · Zbl 0703.68018
[17] Degesys J, Basu P, Redi J (2008) Synchronization of strongly pulse-coupled oscillators with refractory periods and random medium access. In: Proceedings of the SAC 2008, ACM, pp 1976-1980
[18] Dehnert C, Junges S, Katoen JP, Volk M (2017) A storm is coming: a modern probabilistic model checker. In: CAV, Springer, pp 592-600
[19] Delzanno, G., Constraint-based verification of parametrized cache coherence protocols, Form. Methods Syst. Design, 23, 3, 257-301 (2003) · Zbl 1073.68518
[20] Donaldson AF, Miller A (2006) Symmetry reduction for probabilistic model checking using generic representatives. In: ATVA 2006, Springer, Berlin, LNCS, vol 4218, pp 9-23. doi:10.1007/11901914_4 · Zbl 1161.68564
[21] Emerson EA, Trefler RJ (1999) From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: CHARME 1999, Springer, Berlin, LNCS, vol 1703, pp 142-156. doi:10.1007/3-540-48153-2_12 · Zbl 0957.68067
[22] Fatès N (2015) Remarks on the cellular automaton global synchronisation problem. In: Proceedinsg of the AUTOMATA 2015, Springer, LNCS, vol 9099, pp 113-126 · Zbl 1432.68274
[23] Feller, W., An introduction to probability theory and its applications (1968), New York: Wiley, New York · Zbl 0155.23101
[24] Gainer P, Linker S, Dixon C, Hustadt U, Fisher M (2017) Investigating parametric influence on discrete synchronisation protocols using quantitative model checking. In: QEST 2017, Springer, Cham, LNCS, vol 10503, pp 224-239. doi:10.1007/978-3-319-66335-7_14 · Zbl 1420.68127
[25] Gainer P, Linker S, Dixon C, Hustadt U, Fisher M (2018) The power of synchronisation: formal analysis of power consumption in networks of pulse-coupled oscillators. In: 20th international conference on formal engineering methods, ICFEM 2018, pp 160-176. doi:10.1007/978-3-030-02450-5_10
[26] Gusella, R.; Zatti, S., The accuracy of the clock synchronization achieved by TEMPO in Berkeley UNIX 4.3BSD, IEEE Trans Soft Eng, 15, 7, 847-853 (1989)
[27] Hahn EM, Li Y, Schewe S, Turrini A, Zhang L (2014) IscasMC: a web-based probabilistic model checker. In: Proceeding of the FM 2014, Springer, pp 312-317
[28] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal Aspects Comput, 6, 5, 512-535 (1994) · Zbl 0820.68113
[29] Heidarian, F.; Schmaltz, J.; Vaandrager, F., Analysis of a clock synchronization protocol for wireless sensor networks, Theor Comput Sci, 413, 1, 87-105 (2012) · Zbl 1307.68009
[30] Hillston, J.; Tribastone, M.; Gilmore, S., Stochastic process algebras: from individuals to populations, Comput J, 55, 7, 866-881 (2012)
[31] Kemeny, JG; Snell, JL; Knapp, AW, Denumerable Markov chains: with a chapter of Markov random fields by David Griffeath, graduate texts in mathematics (2012), New York: Springer, New York
[32] Kuramoto Y (1975) Self-entrainment of a population of coupled non-linear oscillators. In: International symposium on mathematical problems in theoretical physics, Springer, LNP, vol 39, pp 420-422 · Zbl 0335.34021
[33] Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: SFM 2007, Springer, Berlin, LNCS, vol 4486, pp 220-270. doi:10.1007/978-3-540-72522-0_6 · Zbl 1323.68379
[34] Kwiatkowska M, Norman G, Parker D (2011a) Prism 4.0: verification of probabilistic real-time systems. In: Proceedings of the CAV 2011, Springer, LNCS, vol 6806, pp 585-591
[35] Kwiatkowska M, Parker D, Qu H (2011b) Incremental quantitative verification for markov decision processes. In: international conference on dependable systems and networks, IEEE, pp 359-370
[36] Maróti M, Kusy B, Simon G, Lédeczi A (2004) The flooding time synchronization protocol. In: Proceedings of SenSys 2004, ACM, pp 39-49
[37] MEMSIC, Inc (2017) MICAz wireless measurement system. http://www.memsic.com/userfiles/files/Datasheets/WSN/micaz_datasheet-t.pdf. Accessed 3rd March 2017
[38] Mirollo, RE; Strogatz, SH, Synchronization of pulse-coupled biological oscillators, SIAM J App Math, 50, 6, 1645-1662 (1990) · Zbl 0712.92006
[39] Pagliari R, Scaglione A (2007) Design and implementation of a PCO-based protocol for sensor networks. In: Proceedings of SenSys 2007, pp 387-388. ACM
[40] Parker DA (2003) Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham
[41] Perez-Diaz F, Zillmer R, Groß R (2015) Firefly-inspired synchronization in swarms of mobile agents. In: Proceedings of AAMAS 2015, international foundation for autonomous agents and multiagent systems, pp 279-286
[42] Perez-Diaz F, Trenkwalder SM, Zillmer R, Groß R (2018) Emergence and inhibition of synchronization in robot swarms. In: DARS 2016, Springer, Cham, pp 475-486. doi:10.1007/978-3-319-73008-0_33
[43] Peskin C (1975) Mathematical aspects of heart physiology. Courant Lecture Notes, Courant Institute of Mathematical Sciences, New York University · Zbl 0301.92001
[44] Rhee S, Seetharam D, Liu S (2004) Techniques for minimizing power consumption in low data-rate wireless sensor networks. In: Proceedings of the WCNC 2004, IEEE, pp 1727-1731
[45] Soloveichik, D.; Cook, M.; Winfree, E.; Bruck, J., Computation with finite stochastic chemical reaction networks, Nat Comput, 7, 4, 615-633 (2008) · Zbl 1187.68220
[46] Sommer P, Wattenhofer R (2009) Gradient clock synchronization in wireless sensor networks. In: Proceedings of IPSN 2009, IEEE, pp 37-48
[47] Tyrrell A, Auer G, Bettstetter C (2006) Fireflies as role models for synchronization in ad hoc networks. In: Proceedings of Bionetics 2006, ACM, pp 1-7
[48] Wang, Y.; Nuñez, F.; Doyle, FJ, Energy-efficient pulse-coupled synchronization strategy design for wireless sensor networks through reduced idle listening, IEEE Trans Sig Proc, 60, 10, 5293-5306 (2012) · Zbl 1393.94979
[49] Webster M, Breza M, Dixon C, Fisher M, McCann J (2018) Formal verification of synchronisation, gossip and environmental effects for critical IoT systems. In: Proceedings of AVoCS 2018, EasyChair, EasyChair Preprint no. 377
[50] Werner-Allen G, Tewari G, Patel A, Welsh M, Nagpal R (2005) Firefly-inspired sensor network synchronicity with realistic radio effects. In: Proceedings of SenSys 2005, ACM, pp 142-153
[51] Yick, J.; Mukherjee, B.; Ghosal, D., Wireless sensor network survey, Comput Netw, 52, 12, 2292-2330 (2008)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.