The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators
Authors:
Preprint
Abstract
We assess the power consumption of network synchronisation protocols, particularly the energy required to synchronise all nodes across a network. We use the widely adopted approach 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 assess a range of parameter instantiations and to explore trade-offs between power consumption and time to synchronise. This provides a principled basis for the formal analysis of a much broader range of large-scale network protocols.Keywords
All Related Versions
This publication has 18 references indexed in Scilit:
- Firefly-inspired and robust time synchronization for cognitive radio ad hoc networksComputer Communications, 2015
- Analysis of a clock synchronization protocol for wireless sensor networksTheoretical Computer Science, 2012
- Performability assessment by model checking of Markov reward modelsFormal Methods in System Design, 2010
- Detecting synchronisation of biological oscillators by model checkingTheoretical Computer Science, 2010
- Leader Election in Anonymous Radio Networks: Model Checking Energy ConsumptionLecture Notes in Computer Science, 2010
- Stochastic Model Checking2007
- Symmetry Reduction for Probabilistic Model Checking Using Generic RepresentativesLecture Notes in Computer Science, 2006
- From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking2003
- A theory of timed automataTheoretical Computer Science, 1994
- Chemical Oscillations, Waves, and Turbulence1984