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

Fingerprint

Formal methods
Sampling

Keywords

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

Cite this

Crouzen, P., van de Pol, J. C., Rensink, A., Haverkort, B. R. H. M. (Ed.), Siegle, M. (Ed.), van Steen, M. R. (Ed.), & van Steen, M. (Ed.) (2008). Applying Formal Methods to Gossiping Networks with mCRL and Groove. Performance Evaluation Review, 36(CFP08545-D/3), 7-16. https://doi.org/10.1145/1481506.1481510
Crouzen, P ; van de Pol, Jan Cornelis ; Rensink, Arend ; Haverkort, Boudewijn R.H.M. (Editor) ; Siegle, M. (Editor) ; van Steen, Martinus Richardus (Editor) ; van Steen, M. (Editor). / Applying Formal Methods to Gossiping Networks with mCRL and Groove. In: Performance Evaluation Review. 2008 ; Vol. 36, No. CFP08545-D/3. pp. 7-16.
@article{e73bdeb6dada40dd9f257b67a80fdee6,
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, IR-65245, METIS-255037, EWI-14682",
author = "P Crouzen and {van de Pol}, {Jan Cornelis} and Arend Rensink and Haverkort, {Boudewijn R.H.M.} and M. Siegle and {van Steen}, {Martinus Richardus} and {van Steen}, M.",
note = "10.1145/1481506.1481510",
year = "2008",
month = "12",
doi = "10.1145/1481506.1481510",
language = "English",
volume = "36",
pages = "7--16",
journal = "Performance Evaluation Review",
issn = "0163-5999",
publisher = "Association for Computing Machinery (ACM)",
number = "CFP08545-D/3",

}

Crouzen, P, van de Pol, JC, Rensink, A, Haverkort, BRHM (ed.), Siegle, M (ed.), van Steen, MR (ed.) & van Steen, M (ed.) 2008, 'Applying Formal Methods to Gossiping Networks with mCRL and Groove', Performance Evaluation Review, vol. 36, no. CFP08545-D/3, pp. 7-16. https://doi.org/10.1145/1481506.1481510

Applying Formal Methods to Gossiping Networks with mCRL and Groove. / Crouzen, P; van de Pol, Jan Cornelis; Rensink, Arend; Haverkort, Boudewijn R.H.M. (Editor); Siegle, M. (Editor); van Steen, Martinus Richardus (Editor); van Steen, M. (Editor).

In: Performance Evaluation Review, Vol. 36, No. CFP08545-D/3, 12.2008, p. 7-16.

Research output: Contribution to journalArticleScientificpeer-review

TY - JOUR

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

AU - Crouzen, P

AU - van de Pol, Jan Cornelis

AU - Rensink, Arend

A2 - Haverkort, Boudewijn R.H.M.

A2 - Siegle, M.

A2 - van Steen, Martinus Richardus

A2 - van Steen, M.

N1 - 10.1145/1481506.1481510

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

KW - IR-65245

KW - METIS-255037

KW - EWI-14682

U2 - 10.1145/1481506.1481510

DO - 10.1145/1481506.1481510

M3 - Article

VL - 36

SP - 7

EP - 16

JO - Performance Evaluation Review

JF - Performance Evaluation Review

SN - 0163-5999

IS - CFP08545-D/3

ER -

Crouzen P, van de Pol JC, Rensink A, Haverkort BRHM, (ed.), Siegle M, (ed.), van Steen MR, (ed.) et al. Applying Formal Methods to Gossiping Networks with mCRL and Groove. Performance Evaluation Review. 2008 Dec;36(CFP08545-D/3):7-16. https://doi.org/10.1145/1481506.1481510