|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
Saarland University (GERMANY)
University of Twente (THE NETHERLANDS) |
|---|---|
| Method: |
muCRL
Markov reward models |
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
muCRL GROOVE |
| 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: http://eprints.eemcs.utwente.nl/14682/02/CrouzenVandePolRensink.pdf or from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | 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 Email: [email protected] |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page