Applying Formal Methods to Gossiping Networks with mCRL and Groove

P Crouzen; Jan Cornelis van de Pol; Arend Rensink; Boudewijn R.H.M. Haverkort; M. Siegle; Martinus Richardus van Steen; M. van Steen

doi:10.1145/1481506.1481510

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 journal › Article › Scientific › peer-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 language	English
Pages (from-to)	7-16
Number of pages	10
Journal	Performance Evaluation Review
Volume	36
Issue number	CFP08545-D/3
DOIs	https://doi.org/10.1145/1481506.1481510
Publication status	Published - Dec 2008
Externally published	Yes

Keywords

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

Access to Document

10.1145/1481506.1481510

Cite this

@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 = dec,

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",

}

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 journal › Article › Scientific › peer-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 -

Applying Formal Methods to Gossiping Networks with mCRL and Groove

Abstract

Keywords

Access to Document

Fingerprint

Cite this