Formal Modelling and Verification of Population Protocols

Dominique Méry 1, 2 Mike Poppleton 3
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
3 School of Electronics and Computer Science
ECS - School of Electronics and Computer Science
Abstract : The population protocols of Angluin, Aspnes et al provide a theoretical framework for computability reasoning about algorithms for Mobile Ad-Hoc Networks (MANETs) and Wireless Sensor Networks (WSNs). By developing two example protocols and proving convergence results using the Event- B/RODIN and TLA frameworks, we explore the potential for formal analysis of these protocols.
Complete list of metadatas

https://hal.inria.fr/hal-00813033
Contributor : Dominique Méry <>
Submitted on : Sunday, April 14, 2013 - 7:33:43 PM
Last modification on : Wednesday, September 18, 2019 - 1:26:02 PM

Identifiers

  • HAL Id : hal-00813033, version 1

Collections

Citation

Dominique Méry, Mike Poppleton. Formal Modelling and Verification of Population Protocols. iFM - 10th International Conference on integrated Formal Methods - 2013, Jun 2013, Turku, Finland. ⟨hal-00813033⟩

Share

Metrics

Record views

446