Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols

Ansgar Fehnker, Peng Gao

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    35 Citations (Scopus)

    Abstract

    This paper describes formal probabilistic models of flooding and gossiping protocols, and explores the influence of different modeling choices and assumptions on the results of performance analysis. We use Prism, a model checker for probabilistic systems, for the formal analysis of protocols and small network topologies, and use in addition Monte-Carlo simulation, implemented in Matlab, to establish if the results and effects found during formal analysis extend to larger networks. This combination of approaches has several advantages. The formal model has well defined synchronisation primitives with clear semantics for modeling synchronous and asynchronous communication between nodes. Model checking of the probabilistic model determines exact probabilities and performance bounds, even if the model is non-deterministic; results that cannot be obtained by simulation. However, Monte-Carlo simulation can then be used in addition to study effects that only emerge in larger networks, such as phase transition.
    Original languageEnglish
    Title of host publicationAd-Hoc, Mobile, and Wireless Networks
    Subtitle of host publication5th International Conference, ADHOC-NOW 2006, Ottawa, Canada, August 17-19, 2006, Proceedings
    EditorsThomas Kunz, S. S. Ravi
    PublisherSpringer
    Pages128-141
    Number of pages14
    ISBN (Electronic)978-3-540-37248-6
    ISBN (Print)978-3-540-37246-2
    DOIs
    Publication statusPublished - 2006
    Event5th International Conference on Ad-Hoc, Mobile, and Wireless Networks, ADHOC-NOW 2006 - Ottawa, Canada
    Duration: 17 Aug 200619 Aug 2006
    Conference number: 5

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume4104
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference5th International Conference on Ad-Hoc, Mobile, and Wireless Networks, ADHOC-NOW 2006
    Abbreviated titleADHOC-NOW 2006
    CountryCanada
    CityOttawa
    Period17/08/0619/08/06

    Keywords

    • Source Node
    • Model Check
    • Markov Decision Process
    • Probabilistic Choice
    • Execution Order

    Fingerprint Dive into the research topics of 'Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols'. Together they form a unique fingerprint.

    Cite this