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

    33 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

    Fingerprint

    Network protocols
    Model checking
    Prisms
    Synchronization
    Phase transitions
    Semantics
    Topology
    Communication
    Formal verification
    Monte Carlo simulation
    Statistical Models

    Keywords

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

    Cite this

    Fehnker, A., & Gao, P. (2006). Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. In T. Kunz, & S. S. Ravi (Eds.), Ad-Hoc, Mobile, and Wireless Networks: 5th International Conference, ADHOC-NOW 2006, Ottawa, Canada, August 17-19, 2006, Proceedings (pp. 128-141). (Lecture Notes in Computer Science; Vol. 4104). Springer. https://doi.org/10.1007/11814764_12
    Fehnker, Ansgar ; Gao, Peng. / Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. Ad-Hoc, Mobile, and Wireless Networks: 5th International Conference, ADHOC-NOW 2006, Ottawa, Canada, August 17-19, 2006, Proceedings. editor / Thomas Kunz ; S. S. Ravi. Springer, 2006. pp. 128-141 (Lecture Notes in Computer Science).
    @inproceedings{10ddc5848fd746a59441ccf2e8a0ec4b,
    title = "Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols",
    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.",
    keywords = "Source Node, Model Check, Markov Decision Process, Probabilistic Choice, Execution Order",
    author = "Ansgar Fehnker and Peng Gao",
    year = "2006",
    doi = "10.1007/11814764_12",
    language = "English",
    isbn = "978-3-540-37246-2",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "128--141",
    editor = "Thomas Kunz and Ravi, {S. S.}",
    booktitle = "Ad-Hoc, Mobile, and Wireless Networks",

    }

    Fehnker, A & Gao, P 2006, Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. in T Kunz & SS Ravi (eds), Ad-Hoc, Mobile, and Wireless Networks: 5th International Conference, ADHOC-NOW 2006, Ottawa, Canada, August 17-19, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4104, Springer, pp. 128-141, 5th International Conference on Ad-Hoc, Mobile, and Wireless Networks, ADHOC-NOW 2006, Ottawa, Canada, 17/08/06. https://doi.org/10.1007/11814764_12

    Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. / Fehnker, Ansgar; Gao, Peng.

    Ad-Hoc, Mobile, and Wireless Networks: 5th International Conference, ADHOC-NOW 2006, Ottawa, Canada, August 17-19, 2006, Proceedings. ed. / Thomas Kunz; S. S. Ravi. Springer, 2006. p. 128-141 (Lecture Notes in Computer Science; Vol. 4104).

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

    TY - GEN

    T1 - Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols

    AU - Fehnker, Ansgar

    AU - Gao, Peng

    PY - 2006

    Y1 - 2006

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

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

    KW - Source Node

    KW - Model Check

    KW - Markov Decision Process

    KW - Probabilistic Choice

    KW - Execution Order

    U2 - 10.1007/11814764_12

    DO - 10.1007/11814764_12

    M3 - Conference contribution

    SN - 978-3-540-37246-2

    T3 - Lecture Notes in Computer Science

    SP - 128

    EP - 141

    BT - Ad-Hoc, Mobile, and Wireless Networks

    A2 - Kunz, Thomas

    A2 - Ravi, S. S.

    PB - Springer

    ER -

    Fehnker A, Gao P. Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols. In Kunz T, Ravi SS, editors, Ad-Hoc, Mobile, and Wireless Networks: 5th International Conference, ADHOC-NOW 2006, Ottawa, Canada, August 17-19, 2006, Proceedings. Springer. 2006. p. 128-141. (Lecture Notes in Computer Science). https://doi.org/10.1007/11814764_12