Multi-scale verification of distributed synchronisation
From MaRDI portal
Abstract: 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.
Recommendations
- Synchronizability for Verification of Asynchronously Communicating Systems
- Correct Hardware Design and Verification Methods
- On the complexity of verification of time-sensitive distributed systems
- scientific article; zbMATH DE number 1670505
- Pervasive verification of distributed real-time systems
- Formal verification of Multi-Paxos for distributed consensus
- On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency
Cites work
- scientific article; zbMATH DE number 3471821 (Why is no real title available?)
- scientific article; zbMATH DE number 3524004 (Why is no real title available?)
- scientific article; zbMATH DE number 1487862 (Why is no real title available?)
- scientific article; zbMATH DE number 3249395 (Why is no real title available?)
- A logic for reasoning about time and reliability
- A theory of timed automata
- Analysis of a clock synchronization protocol for wireless sensor networks
- Chemical reaction network designs for asynchronous logic circuits
- Computation in networks of passively mobile finite-state sensors
- Computation with finite stochastic chemical reaction networks
- Constraint-based verification of parameterized cache coherence protocols
- Detecting synchronisation of biological oscillators by model checking
- Energy-Efficient Pulse-Coupled Synchronization Strategy Design for Wireless Sensor Networks Through Reduced Idle Listening
- Investigating parametric influence on discrete synchronisation protocols using quantitative model checking
- Probabilistic clock synchronization
- Programming discrete distributions with chemical reaction networks
- Remarks on the cellular automaton global synchronisation problem
- Stochastic model checking
- Symbolic Counter Abstraction for Concurrent Software
- Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives
- Synchronization of Pulse-Coupled Biological Oscillators
Cited in
(3)
This page was built for publication: Multi-scale verification of distributed synchronisation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225471)
