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).
CITATION STYLE
André, É., Fribourg, L., Mota, J. M., & Soulat, R. (2019). Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11388 LNCS, pp. 409–424). Springer Verlag. https://doi.org/10.1007/978-3-030-11245-5_19
Mendeley helps you to discover research relevant for your work.