Semantic Analysis of Gossip Protocols for Wireless Sensor Networks
Gossip protocols have been proposed as a robust and efficient method for disseminating information throughout large-scale networks. In this paper, the authors propose a compositional analysis technique to study formal probabilistic models of gossip protocols in the context of wireless sensor networks. They introduce a simple probabilistic timed process calculus for modelling wireless sensor networks. A simulation theory is developed to compare probabilistic protocols that have similar behaviour up to a certain probability. This theory is used to prove a number of algebraic laws which revealed to be very effective to evaluate the performances of gossip networks with and without communication collisions.