Formal verification and simulation for performance analysis for probabilistic broadcast protocols

Ansgar Fehnker, Peng Gao

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

41 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
Place of PublicationBerlin
PublisherSpringer, Springer Nature
Pages128-141
Number of pages14
ISBN (Print)9783540372462, 3540372466
DOIs
Publication statusPublished - 2006
Externally publishedYes
Event5th International Conference on Ad-Hoc, Mobile, and Wireless Networks, ADHOC-NOW 2006 - Ottawa, Canada
Duration: 17 Aug 200619 Aug 2006

Publication series

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

Conference

Conference5th International Conference on Ad-Hoc, Mobile, and Wireless Networks, ADHOC-NOW 2006
Abbreviated titleADHOC-NOW2006
Country/TerritoryCanada
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