2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering (2009)
July 29, 2009 to July 31, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2009.9
Population protocols are an elegant model recently introduced for distributed algorithms running in large and unreliable networks of tiny mobile agents. Correctness proofs of such protocols involve subtle arguments on infinite sequences of events. We propose a general formalization of self-stabilizing population protocols with the Coq proof assistant. It is used in reasoning about a concrete protocol for leader election in complete graphs. The protocol is formally proved to be correct for networks of arbitrarily large size. To this end we develop an appropriate theory of infinite sequences, including results for reasoning on abstractions. In addition, we provide a constructive correctness proof for a leader election protocol in directed rings. An advantage of using a constructive setting is that we get more informative proofs on the scenarios that converge to the desired configurations.
formal verification; population protocols; self-stabilization; proof assistant; Coq
J. Monin and Y. Deng, "Verifying Self-stabilizing Population Protocols with Coq," 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering(TASE), Tianjin, China, 2009, pp. 201-208.