Applying Formal Methods to Gossiping Networks with mCRL and Groove

P Crouzen, Jan Cornelis van de Pol, Arend Rensink, Boudewijn R.H.M. Haverkort (Editor), M. Siegle (Editor), Martinus Richardus van Steen (Editor), M. van Steen (Editor)

Research output: Contribution to journalArticleScientificpeer-review

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].
Original languageEnglish
Pages (from-to)7-16
Number of pages10
JournalPerformance Evaluation Review
Volume36
Issue numberCFP08545-D/3
DOIs
Publication statusPublished - Dec 2008
Externally publishedYes

Keywords

  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • IR-65245
  • METIS-255037
  • EWI-14682

Fingerprint Dive into the research topics of 'Applying Formal Methods to Gossiping Networks with mCRL and Groove'. Together they form a unique fingerprint.

Cite this