Applying Formal Methods to Gossiping Networks with mCRL and Groove

Research output: Contribution to journalArticleAcademicpeer-review

18 Downloads (Pure)

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
JournalSIGMETRICS performance evaluation review
Volume36
Issue number3
DOIs
Publication statusPublished - Dec 2008

Fingerprint

Formal methods
Sampling

Keywords

  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

Cite this

@article{801a36a684cb4d89938240da5dba9faf,
title = "Applying Formal Methods to Gossiping Networks with mCRL and Groove",
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].",
keywords = "FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS",
author = "Pepijn Crouzen and {van de Pol}, Jaco and Arend Rensink",
year = "2008",
month = "12",
doi = "10.1145/1481506.1481510",
language = "English",
volume = "36",
pages = "7--16",
journal = "SIGMETRICS performance evaluation review",
issn = "0163-5999",
publisher = "Association for Computing Machinery (ACM)",
number = "3",

}

Applying Formal Methods to Gossiping Networks with mCRL and Groove. / Crouzen, Pepijn; van de Pol, Jaco; Rensink, Arend.

In: SIGMETRICS performance evaluation review, Vol. 36, No. 3, 12.2008, p. 7-16.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Applying Formal Methods to Gossiping Networks with mCRL and Groove

AU - Crouzen, Pepijn

AU - van de Pol, Jaco

AU - Rensink, Arend

PY - 2008/12

Y1 - 2008/12

N2 - 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].

AB - 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].

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

U2 - 10.1145/1481506.1481510

DO - 10.1145/1481506.1481510

M3 - Article

VL - 36

SP - 7

EP - 16

JO - SIGMETRICS performance evaluation review

JF - SIGMETRICS performance evaluation review

SN - 0163-5999

IS - 3

ER -