Multi-scale verification of distributed synchronisation
- PDF / 986,019 Bytes
- 51 Pages / 439.37 x 666.142 pts Page_size
- 50 Downloads / 150 Views
Multi-scale verification of distributed synchronisation Paul Gainer1 · Sven Linker1 Michael Fisher1
· Clare Dixon1,2
· Ullrich Hustadt1
·
© The Author(s) 2020
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. Keywords Synchronisation · Pulse-coupled oscillators · Abstraction · Probabilistic verification · Weak bisimulation
1 Introduction Small computing devices comprising networks, be it commercial wireless sensor networks, or communicating devices in the Internet of Things, are becoming increasingly common. However, to enable these devices to communicate efficiently, they have to employ methods to use the shared communication medium while avoiding conflicting messages on this medium,
This work was supported by the Sir Joseph Rotblat Alumni Scholarship at Liverpool and the Engineering and Physical Sciences Research Council, under Grants EP/N007565/1 (S4: Science of Sensor Systems Software), EP/L024845/1 (Verifiable Autonomy), and the FAIR-SPACE (EP/R026092/1) and RAIN (EP/R026084/1) RAI Hubs. Extended author information available on the last page of the article
123
Formal Methods in System Design
in particular in the form of collisions. Collisions occur if two or more devices simultaneously try to access the communication medium, and often result in neither message being delivered. Several protocols to organise shared medium access have been developed and analysed [1,51]. These protocols typically identify a common time frame and divide this frame into slots associated to each node. Thus every node has an allocated time slot that it may use
Data Loading...
