Applying Formal Methods to Gossiping Networks with mCRL and Groove

    Research output: Contribution to journalArticleAcademicpeer-review

    20 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

    Keywords

    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

    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