Applying Formal Methods to Gossiping Networks with mCRL and Groove

Share/Save/Bookmark

Crouzen, P. and Pol van de, J.C. and Rensink, A. (2008) Applying Formal Methods to Gossiping Networks with mCRL and Groove. ACM SIGMETRICS Performance Evaluation Review, 36 (3). pp. 7-16. ISSN 0163-5999

[img]
Preview
PDF
249Kb
[img]
Preview
PDF
209Kb
Abstract:In this paper we explore the practical possibilities of using formal methods to analyze gossiping networks. In particular, we use mCRL and Groove to model the peer sampling service, and analyze it through a series of model transformations to CTMCs and finally MRMs. Our tools compute the expected value of various network quality indicators, such as average path lengths, over all possible system runs. Both transient and steady state analysis are supported. We compare our results with the simulation and emulation results found in [10].
Item Type:Article
Copyright:© 2008 ACM
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/65245
Official URL:http://dx.doi.org/10.1145/1481506.1481510
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 255037