Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking
arXiv:1812.08949 · doi:10.1007/978-3-030-11245-5_19
Abstract
The election of a leader in a network is a challenging task, especially when the processes are asynchronous, i.e., execute an algorithm with time-varying periods. Thales developed an industrial election algorithm with an arbitrary number of processes, that can possibly fail. In this work, we prove the correctness of a variant of this industrial algorithm. We use a method combining abstraction, the SafeProver solver, and a parametric timed model-checker. This allows us to prove the correctness of the algorithm for a large number p of processes (p=5000).
This is the author version of the manuscript of the same name published in the proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2019)