The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators | SpringerLink
Skip to main content
Springer Nature Link
Log in

The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11232))

Included in the following conference series:

Abstract

Nature-inspired synchronisation protocols have been widely adopted to achieve consensus within wireless sensor networks. We analyse the power consumption of such protocols, particularly the energy required to synchronise all nodes across a network. We use the model of bio-inspired, pulse-coupled oscillators to achieve network-wide synchronisation and provide an extended formal model of just such a protocol, enhanced with structures for recording energy usage. Exhaustive analysis is then carried out through formal verification, utilising the PRISM model-checker to calculate the resources consumed on each possible system execution. This allows us to investigate a range of parameter instantiations and the trade-offs between power consumption and time to synchronise. This provides a principled basis for the formal analysis of a broader range of large-scale network protocols.

This work was supported by the Sir Joseph Rotblat Alumni Scholarship at Liverpool, the EPSRC Research Programme EP/N007565/1 Science of Sensor Systems Software and the EPSRC Research Grant EP/L024845/1 Verifiable Autonomy. The authors would like to thank the Networks Sciences and Technology Initiative (NeST) of the University of Liverpool for the use of their computing facilities and David Shield for the corresponding technical support.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    The scripts, along with the verification results, can be found at https://github.com/PaulGainer/mc-bio-synch/tree/master/energy-analysis.

  2. 2.

    While most individual model checking runs finished within a minute, the cumulative model checking time over all analysed models was very large. The results shown in Fig. 3a already amount to 80 distinct runs.

  3. 3.

    Within Prism this can be achieved by using the filter construct.

References

  1. Albers, S.: Energy-efficient algorithms. Commun. ACM 53(5), 86–96 (2010)

    Article  Google Scholar 

  2. Bartocci, E., Corradini, F., Merelli, E., Tesei, L.: Detecting synchronisation of biological oscillators by model checking. Theor. Comput. Sci. 411(20), 1999–2018 (2010)

    Article  MathSciNet  Google Scholar 

  3. Bojic, I., Lipic, T., Kusek, M.: Scalability issues of firefly-based self-synchronization in collective adaptive systems. In: Proceedings of SASOW 2014, pp. 68–73. IEEE (2014)

    Google Scholar 

  4. Bortolussi, L., Hillston, J.: Efficient checking of individual rewards properties in Markov population models. In: QAPL 2015. EPTCS, vol. 194, pp. 32–47. Open Publishing Association (2015)

    Google Scholar 

  5. Donaldson, A.F., Miller, A.: Symmetry reduction for probabilistic model checking using generic representatives. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 9–23. Springer, Heidelberg (2006). https://doi.org/10.1007/11901914_4

    Chapter  Google Scholar 

  6. Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48153-2_12

    Chapter  Google Scholar 

  7. Fatès, N.: Remarks on the cellular automaton global synchronisation problem. In: Kari, J. (ed.) AUTOMATA 2015. LNCS, vol. 9099, pp. 113–126. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47221-7_9

    Chapter  MATH  Google Scholar 

  8. Gainer, P., Dixon, C., Hustadt, U.: Probabilistic model checking of ant-based positionless swarming. In: Alboul, L., Damian, D., Aitken, J.M.M. (eds.) TAROS 2016. LNCS (LNAI), vol. 9716, pp. 127–138. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40379-3_13

    Chapter  Google Scholar 

  9. Gainer, P., Linker, S., Dixon, C., Hustadt, U., Fisher, M.: Investigating parametric influence on discrete synchronisation protocols using quantitative model checking. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 224–239. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66335-7_14

    Chapter  Google Scholar 

  10. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. FAC 6(5), 512–535 (1994)

    MATH  Google Scholar 

  11. Heidarian, F., Schmaltz, J., Vaandrager, F.: Analysis of a clock synchronization protocol for wireless sensor networks. Theor. Comput. Sci. 413(1), 87–105 (2012)

    Article  MathSciNet  Google Scholar 

  12. Konishi, K., Kokame, H.: Synchronization of pulse-coupled oscillators with a refractory period and frequency distribution for a wireless sensor network. Chaos: Interdisciplinary J. Nonlinear Sci. 18(3) (2008)

    Article  Google Scholar 

  13. Kuramoto, Y.: Self-entrainment of a population of coupled non-linear oscillators. In: Araki, H. (ed.) International Symposium on Mathematical Problems in Theoretical Physics. LNP, vol. 39, pp. 420–422. Springer, Heidelberg (1975)

    Chapter  Google Scholar 

  14. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  15. Lucarelli, D., Wang, I.J., et al.: Decentralized synchronization protocols with nearest neighbor communication. In: Proceedings of SenSys 2004, pp. 62–68. ACM (2004)

    Google Scholar 

  16. MEMSIC Inc.: MICAz datasheet. www.memsic.com/userfiles/files/Datasheets/WSN/micaz_datasheet-t.pdf. Accessed 15 Jan 2018

  17. Mirollo, R.E., Strogatz, S.H.: Synchronization of pulse-coupled biological oscillators. SIAM J. Appl. Math. 50(6), 1645–1662 (1990)

    Article  MathSciNet  Google Scholar 

  18. Peskin, C.: Mathematical aspects of heart physiology. Courant Lecture Notes , Courant Institute of Mathematical Sciences, New York University (1975)

    Google Scholar 

  19. Rhee, I.K., Lee, J., Kim, J., Serpedin, E., Wu, Y.C.: Clock synchronization in wireless sensor networks: an overview. Sensors 9(1), 56–85 (2009)

    Article  Google Scholar 

  20. Rhee, S., Seetharam, D., Liu, S.: Techniques for minimizing power consumption in low data-rate wireless sensor networks. In: Proceedings of WCNC 2004, pp. 1727–1731. IEEE (2004)

    Google Scholar 

  21. Soua, R., Minet, P.: A survey on energy efficient techniques in wireless sensor networks. In: Proceedings of WMNC 2011, pp. 1–9. IEEE (2011)

    Google Scholar 

  22. Wang, Y., Nuñez, F., Doyle, F.J.: Energy-efficient pulse-coupled synchronization strategy design for wireless sensor networks through reduced idle listening. IEEE Trans. Sig. Process. 60(10), 5293–5306 (2012)

    Article  MathSciNet  Google Scholar 

  23. Yick, J., Mukherjee, B., Ghosal, D.: Wireless sensor network survey. Comput. Netw. 52(12), 2292–2330 (2008)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Liverpool, Liverpool, UK

    Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt & Michael Fisher

Authors
  1. Paul Gainer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sven Linker
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Clare Dixon
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ullrich Hustadt
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Michael Fisher
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sven Linker .

Editor information

Editors and Affiliations

  1. University of Auckland, Auckland, New Zealand

    Jing Sun

  2. Peking University, Beijing, China

    Meng Sun

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

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: Sun, J., Sun, M. (eds) Formal Methods and Software Engineering. ICFEM 2018. Lecture Notes in Computer Science(), vol 11232. Springer, Cham. https://doi.org/10.1007/978-3-030-02450-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02450-5_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02449-9

  • Online ISBN: 978-3-030-02450-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation