P.Gainer, S. Linker, C. Dixon, U. Hustadt, M. Fisher (2017b): ``Investigating Parametric Influence on Discrete Synchronisation Protocols Using Quantitative Model Checking.'' In N. Bertrand and L. Bortolussi, editors, Proceedings of the 14th International Conference on Quantitative Evaluation of Systems (QEST 2017), [Berlin, Germany, 5-7 July 2017], pp. 224-239. LNCS 10503, Springer, 2017.
Abstract, BibTeX, PDF (© Springer).

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.

Maintained by Ullrich Hustadt, U.Hustadt@liverppol.ac.uk, last updated Monday, 02-Apr-2018 21:10:15 BST © 2018 by Ullrich Hustadt.