Database of Case Studies Achieved Using CADP

Gossiping Networks

Organisation: Saarland University (GERMANY)
University of Twente (THE NETHERLANDS)

Method: muCRL
Markov reward models

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Distributed Systems.

Period: 2008

Size: n/a

Description: Gossiping networks provide a novel way of constructing distributed systems. A gossiping network consists of a large number of simple nodes, which have a limited view of the network. The idea is that information is dissipated in a gossiping style, i.e., every node communicates its information to a small number of other nodes in the same way people spread gossip through a community. This style of communication is also called epidemic for its similarity to a disease spreading through a population. Gossiping networks have been used successfully in a number of applications.

These networks are inherently dynamic, because nodes may enter or leave the system, and their connections may vary over time. Furthermore, gossiping network models combine concurrency and probabilistic behaviour in a timed setting, which leads to modeling and analysis complications. This work deals with the usage of formal methods to analyze gossiping networks. More precisely, it is investigated how the gossiping networks can be modeled, how well explicit-state model checking scales up with the size of the networks, and whether the results obtained are useful in making design decisions.

Gossiping networks are modeled using the muCRL process algebraic language, encoding the dynamic aspects by means of static data types. The GROOVE tool based on graph transformations is used for exploring symmetry reduction of gossiping networks. Then, the muCRL specification is transformed into a continuous-time Markov chain (CTMC) by combining concurrent, probabilistic and stochastic behaviours along the lines of the MLOTOS process algebraic language. Each state of the CTMC is labeled with a directed graph representing the state of the gossiping network. Three different Markov reward models (MRMs) are then produced from the CTMC, having as reward structure the indegree variance, the average shortest path, and the clustering coefficient, respectively.

The analysis of the resulting MRMs is carried out by first computing, using the BCG_TRANSIENT and BCG_STEADY tools of CADP, the probability to reside in each state at certain time points and on the long run. Next, each MRM is checked seperately, using an extension to the CSRL logic implemented using the XTL model checker of CADP. This extension provides both instantaneous rewards (the expected value of one of the measures at some time point) and the long run reward rate (the expected average value of the measures on the long run). The results found for small-size configurations (up to 7 nodes) confirm previously published results obtained using simulation and emulation.

Conclusions: This study showed that gossiping networks can be analyzed using formal methods, by combining process algebraic, graph transformation, and stochastic model checking features. The results found even for small models suggest that small-scale analysis can lead to insights in the behaviour of large-scale networks. Also, the traceability of the formal models can give a deeper understanding of the emergent behaviour of a gossiping network.

Publications: [Crouzen-vandePol-Rensink-08] Pepijn Crouzen, Jaco van de Pol, and Arend Rensink. "Applying Formal Methods to Gossiping Networks with mCRL and Groove". SIGMETRICS Performance Evaluation Review 36(3):7-16, 2008.
Available on-line at:
or from our FTP site in PDF or PostScript

Prof. Jaco van de Pol
Chair Formal Methods and Tools
Department of Computer Science
University of Twente
P.O. Box 217
7500 AE Enschede
The Netherlands
Tel: +31 (0)53 489 3017
Fax: +31 (0)53 489 3247

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 19 09:12:04 2016.

Back to the CADP case studies page