Applying Formal Methods to Gossiping Networks with mCRL and Groove

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

Preview

PDF
249Kb

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:	Formal Methods and Tools (FMT)
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

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 255037