Title
Analysis of a gossip protocol in PRISM
Abstract
Gossip protocols have been proposed as a robust and efficient method for disseminating information throughout dynamically changing networks. We present an analysis of a gossip protocol using probabilistic model checking and the tool PRISM. Since the behaviour of these protocols is both probabilistic and nondeterministic in nature, this provides a good example of the exhaustive, quantitative analysis that probabilistic model checking techniques can provide. In particular, we compute minimum and maximum values, representing the best- and worst-case performance of the protocol under any scheduling, and investigate both their relationship with the average values that would be obtained through simulation and the precise scheduling which achieve these values.
Year
DOI
Venue
2008
10.1145/1481506.1481511
SIGMETRICS Performance Evaluation Review
Keywords
Field
DocType
quantitative analysis,gossip protocol
Nondeterministic algorithm,Scheduling (computing),Computer science,Real-time computing,Theoretical computer science,Dissemination,Probabilistic logic,Gossip protocol,Probabilistic model checking,Distributed computing
Journal
Volume
Issue
Citations 
36
3
28
PageRank 
References 
Authors
1.24
15
3
Name
Order
Citations
PageRank
Marta Z. Kwiatkowska16118322.21
Gethin Norman24163193.68
David Parker34018184.00