The paper is focused on the Trickle algorithm as it receives an increasing interest in the regulation of information dissemination among IoT devices. The algorithm uses time-control on broadcast suppression in order to minimize message exchanges and save batteries of those small devices, while still being able to quickly spread new information among the network. Such information may be critical such as bug patches or security updates. In this paper, timed behavioural models for Trickle are proposed together with verification of certain key properties of the algorithm on those developed models. The aim is to explore fast, reliable and fair dissemination capabilities of the algorithm.
展开▼
